A comment and question for users of Vim and HOL4: (0. If you don't know about the vim mode, ask :))
1. Folding: I just found out about :set foldmethod=indent. If you have very large proof scripts where each subgoal's proof is indented, this can make it much easier to view and navigate around the whole proof. (Incidentally I recommend using >- (THEN1) and doing each subgoal separately rather than THENL, for various reasons.) 2. Syntax highlighting, and other syntax awareness: The default sml.vim highlighting file and Vim's default understanding of things like what counts as a valid identifier are quite bad at Standard ML (and at HOL scripts a fortiori). Is there anyone on this list who might be closer to having the requisite expertise to improve these than me? Cheers, Ramana ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
