Dear everyone,
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.
"
Each *face* (Emacs terminology) is controlled by its own customization
setting. You can display a list of all of them using the customize menu:
Proof General -> Advanced -> Customize -> Faces -> Proof Faces.
"
I have modified "proof-site.el" , omit the ";;"before hol4, which makes hol4
function enable.
What is wrong with my operation? Please help me! Looking forward to your
reply.
yours
xiaoyu
------------------------------------------------------------------------------
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
