On 18/06/10 15:57, xiaoyu xu wrote: > I have installed ML and HOL4 in windows. How can I prove theorems? I am > a new user of HOL4.
> I have also installed ML HOL4 proofgeneral GNU emacs in Linux system > Fedora. I can't find "proofgeneral"in menu. HOL4 doesn't work with Proof General. If you have emacs installed, I recommend using the emacs-mode, which has a little documentation at http://hol.sourceforge.net/hol-mode.html Michael ------------------------------------------------------------------------------ ThinkGeek and WIRED's GeekDad team up for the Ultimate GeekDad Father's Day Giveaway. ONE MASSIVE PRIZE to the lucky parental unit. See the prize list and enter to win: http://p.sf.net/sfu/thinkgeek-promo _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
