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

[Florian Haftmann]

Hi,

> *** 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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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