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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
