Hi Fellows
Visiting the HOL world after a long time. Installed HOL under Linux (RHEL 3 and
also on Mac OSX-Intel), looks like a clean installation. Most basic libraries
load and work well (including HolSatLib) except for HolSmtLib.
When I load the HolSmtLib at the HOL prompt, I get the following error and HOL
crashes after this error.
What am I missing here?
Thanks in advance
Ashish
---------------------------------------------------------------------
HOL-4 [Kananaskis 7 (stdknl, built Fri Oct 14 00:00:54 2011)]
For introductory HOL help, type: help "hol";
---------------------------------------------------------------------
[loading theories and proof tools ************** ]
[closing file "/Users/ashish/HOL/tools/end-init-boss.sml"]
- load "HolSmtLib";;
! Uncaught exception:
! Chr
- - quit();
Uncaught exception: Chr
ashish$
------------------------------------------------------------------------------
Write once. Port to many.
Get the SDK and tools to simplify cross-platform app development. Create
new or port existing apps to sell to consumers worldwide. Explore the
Intel AppUpSM program developer opportunity. appdeveloper.intel.com/join
http://p.sf.net/sfu/intel-appdev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
