Hi
I am having difficulty in getting the pretty-printer to work properly
in a recent installation of HOL4K6 on my sun workstation with Solaris
10. Quantifiers and operators are not displayed properly by the
pretty-printer (both in xterm and inside Emacs). Here is a sample of
the pretty-printer output:
-----------------------------------------
val IN_BIGUNION =
|- x sos. x  BIGUNION sos  s. x  s  s  sos :
thm
val GSPEC_AND = |- P Q. {x | P x  Q x} = {x | P x}  {x | Q
x} : thm
val INSERT_UNION_EQ = |- ÔêÇx s t. (x INSERT s) Ôê¬ t = x INSERT s
Ôê¬ t :
thm
val INTER_COMM = |- s t. s  t = t  s : thm
val MIN_SET_DEF = |- MIN_SET = $LEAST : thm
val NOT_PSUBSET_EMPTY = |- ÔêÇs. ?¼(s Ôèé Ôêà) : thm
val PSUBSET_INSERT_SUBSET =
|- s t. s  t  x. x  s  x INSERT s  t : thm
val COMPL_INTER = |- (x  COMPL x = )  (COMPL x  x =
Ôêà) : thm
val INSERT_COMM = |- x y s. x INSERT y INSERT s = y INSERT x
INSERT s :
thm
val INTER_EMPTY = |- (s.   s = )  s. s   =
Ôêà : thm
val CROSS_DEF = |- ÔêÇP Q. P ?ù Q = {p | FST p Ôêê P Ôêº SND p Ôêê
Q} : thm
val CARD_EQ_0 = |- s. FINITE s  ((CARD s = 0)  (s = )) :
thm
val DISJOINT_EMPTY = |- s. DISJOINT  s  DISJOINT s  :
thm
val CHOICE_INSERT_REST = |- s. s    (CHOICE s INSERT
REST s = s)
: thm
val DELETE_INTER = |- s t x. (s DELETE x)  t = s  t DELETE
x : thm
val IMAGE_INTER = |- f s t. IM
---------------------------------------------------
I have also tried installing/compiling HOL4K6 on PCs with windows
(vista, windows7) and Linux (SUSE) operating systems and experience
the same problem with the pretty-printer. Everything seems okay on
cygwin though, that is, it works exactly as its described in "Release
Notes -> New features". I am very sure that I have followed the
instruction for building HOL from sources exactly and am wondering
what can I do to get the pretty-printer to display information
correctly?
Thanks
Naeem
------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing.
http://p.sf.net/sfu/novell-sfdev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
