[isabelle] Automaton example




What happens if you load the attached fragment of
Isabelle2005/src/HOLCF/IOA/Modelcheck/Cockpit.thy like this:

  $ Isabelle2005/bin/isabelle IOA
  ML> use_thy "Test";

Make double sure that this is really the IOA image, not just HOL.


If I execute "isabelle IOA" it returns the error:
Unknown logic "IOA" -- no heap file found in:
/home/pozzani/isabelle/heaps/polyml-4.1.4_x86-linux
/home/pozzani/Isabelle/Isabelle2005/heaps/polyml-4.1.4_x86-linux

And if I load HOLCF and so Test, isabelle returns the syntax error:
*** Outer syntax error: end of input expected,
*** but keyword "=" was found
where the "=" is in the second datatype definition.

Have not I installed correctly Isabelle (version 2005)?

Thanks
Gabriele




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.