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

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


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