(global-set-key (kbd "C-c C-d") 'ml4pg-export-theorem)
(global-set-key (kbd "C-c C-e") 'ml4pg-save-file-conventions1)
(global-set-key (kbd "C-c m") 'ml4pg-show-clusters-of-theorem)
(global-set-key (kbd "C-c C-SPC") 'ml4pg-extract-feature-theorems)
(global-set-key (kbd "C-c c") 'ml4pg-show-clusters)
(global-set-key (kbd "C-c e") 'ml4pg-extract-feature-theorems-dynamic)
(global-set-key (kbd "C-c d") 'ml4pg-show-clusters-dynamic)
(global-set-key (kbd "C-c a") 'ml4pg-change-algorithm-interactive)
(global-set-key (kbd "C-c g") 'ml4pg-change-granularity-interactive)
(global-set-key (kbd "C-c f") 'ml4pg-change-frequency-interactive)
(global-set-key (kbd "C-c i") 'ml4pg-change-iterative-interactive)
(global-set-key (kbd "C-c C-m") 'ml4pg-proof-assert-next-command-interactive3)
(global-set-key (kbd "C-c n") 'ml4pg-save-numbers)