Hi Xiaoyu,
There's a "quick-start" document at
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf
and the HOL4 release has extensive documentation
in the Manual directory.
Konrad.
On Jun 18, 2010, at 12:57 AM, xiaoyu xu wrote:
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
------------------------------------------------------------------------------
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
