[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:

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)?


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