Re: [isabelle] libisabelle for Isabelle2015?



Hi Lars,

I was too optimistic ...

There are two ways to fix this: (1) Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or (2) move
the theory files from libisabelle to the Isac repository and list it
in its "src/Tools/isac/ROOT" file.
We prefer (1), because we still want to keep apart libisabelle and Isac.
This works now [...]
Now I'm looking forward to completion of embedding on the ML-side with
great pleasure

... because I found myself with strange errors, which probably are caused by
faulty settings [1]. Correction of the settings is tricky if we want to keep
our repository clean. So I'd prefer to start from scratch with Isabelle2015.

However, trying

   Isabelle2015$ ./bin/isabelle jedit -l HOL ~/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy &

causes the error

   Undefined ML antiquotation: "command_spec"â

Do you have time to update to Isabelle2015 ?

Walther


[1] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00122.html





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