John, just to check, on the same machine, I installed the earlier
version (ocaml 3.09.1 with presumably camlp4) without any trouble.
cd ocaml-3.09.1
./configure -prefix /rhome/2/richter/HOL-Light309
make world.opt
make install
I put $HOME/HOL-Light309/bin and $HOME/HOL-Light309/lib on the front
of my PATH and LD_LIBRARY_PATH variables. Then
cd hol_light
make
no error, so I ran my miz3 Tarski code
hol_light> ocaml
#use "hol.ml";;
paste in file
[....]
val ( I1_THM ) : thm =
|- !a b x y.
~(a = b)
==> ~(x = y)
==> a on_line x,y
==> b on_line x,y
==> x,y equal_line a,b
I never get tired of looking that output!
--
Best,
Bill
------------------------------------------------------------------------------
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
