Re: [isabelle] libisabelle: embedding on ML-side



Hi Lars,

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, however, with ugly absolute paths:
/-------------------------------------------------------------------
theory Protocol
imports
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec"
  "~~/src/Tools/isac/Frontend/Frontend"
:
--------------------------------------------------------------------/

Now I'm looking forward to completion of embedding on the ML-side with great pleasure,

Walther




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