> isabelle: ae7c11573922 tip > afp: 1bffa6708aea tip > *** [line 5 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory "WordDecl" (line 3 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/ROOT") > *** [line 11 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory "Sparc_Instruction" > *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy") > *** [line 11 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_State.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory "Sparc_State" > *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy") > *** [line 11 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory "Sparc_Types" > *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy") > *** The error(s) above occurred in session "SPARCv8" (line 3 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/ROOT")
-- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
