Hello everyone, I am currently running into some technical "difficulties" with using HOL4:
I found that the emacs sml-mode binds the return key to "newline-and-indent" and I cannot find a way to remove this binding. Problem being that emacs keeps indenting my tactic proofs totally weird, so I would favour being able to indent only on my own. So far, I tried deactivating it similar to what worked for removing tab-indentation (setq default-tab-width 4) (setq-default indent-tabs-mode nil) (global-set-key (kbd "TAB") 'self-insert-command) by setting (global-set-key (kbd "RET") 'newline) Unfortunately this does not work. Can someone help me with this issue with some elisp? Thanks in advance. Best regards, Heiko ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
