[isabelle-dev] how to run the SET protocol..

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jul 2 13:50:29 CEST 2010


> *** Theory loader: failed to load "Public_SET" (unresolved "Event_SET")
> *** Theory loader: failed to load "Event_SET" (unresolved "Message_SET")
> *** Theory loader: failed to load "Message_SET" (unresolved "Nat_Bijection")
> *** Inner lexical error at: × nat (line 15 of "/home/pho
> thar/Nat_Bijection.thy")
> *** Failed to parse type (line 15 of "/home/pho thar/Nat_Bijection.thy")
> *** The error(s) above occurred in document antiquotation: "typ" (line
> 15 of "/home/pho thar/Nat_Bijection.thy")
> *** At command "subsection" (line 15 of "/home/pho thar/Nat_Bijection.thy").
> *** At command "theory".

it seems to be the case that you have in your working directory a broken
theory Nat_Bijection.thy which shadows the right one from the Isabelle
library.  Can you check what happens after you rename this?

Hope this helps,



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100702/df52ed74/attachment.sig>

More information about the isabelle-dev mailing list