[isabelle-dev] AFP broken

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Oct 19 20:23:14 CEST 2016


> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161019/7995141e/attachment.asc>


More information about the isabelle-dev mailing list