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

[see sar]

hi

i m trying to run the example of SET protocol in Isabelle but i can't run
it... it came out with the errors.

*** 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".

Can anyone pls tell me, how to run that sample SET protocol?

tnks
see rockyy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100702/8aa7d607/attachment-0002.html>