Changes

Summary

merge from afp-2016
adjust SPARCv8 timeout for single-core runs
new entry SPARCv8
add Source_Coding_Theorem to ROOTS
new entry: Source_Coding_Theorem

Changeset 7231:1bffa6708aea by kleing: merge from afp-2016
Changeset 7230:c6514fe0c053 by gerwin klein _gerwin.klein@data61.csiro.au_: adjust SPARCv8 timeout for single-core runs
The file was modified	`thys/SPARCv8/ROOT` (diff)
Changeset 7229:5b5317f08c2c by gerwin klein _gerwin.klein@data61.csiro.au_: new entry SPARCv8
The file was added	`thys/SPARCv8/ROOT`
The file was added	`thys/SPARCv8/SparcModel_MMU/MMU.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/RegistersOps.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Code_Gen.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Init_State.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Model.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_State.thy`
The file was added	`thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy`
The file was added	`thys/SPARCv8/document/root.tex`
The file was added	`thys/SPARCv8/lib/Lib.thy`
The file was added	`thys/SPARCv8/lib/WordDecl.thy`
The file was added	`thys/SPARCv8/lib/wp/DetMonad.thy`
The file was added	`thys/SPARCv8/lib/wp/DetMonadLemmas.thy`
The file was added	`web/entries/SPARCv8.shtml`
The file was modified	`metadata/metadata` (diff)
The file was modified	`metadata/topics` (diff)
The file was modified	`thys/ROOTS` (diff)
The file was modified	`web/index.shtml` (diff)
The file was modified	`web/topics.shtml` (diff)
Changeset 7228:3f1bc669484f by gerwin klein _gerwin.klein@data61.csiro.au_: add Source_Coding_Theorem to ROOTS
The file was modified	`thys/ROOTS` (diff)
Changeset 7227:b215cc1b3bd4 by gerwin klein _gerwin.klein@nicta.com.au_: new entry: Source_Coding_Theorem
The file was added	`thys/Source_Coding_Theorem/ROOT`
The file was added	`thys/Source_Coding_Theorem/Source_Coding_Theorem.thy`
The file was added	`thys/Source_Coding_Theorem/document/root.bib`
The file was added	`thys/Source_Coding_Theorem/document/root.tex`
The file was added	`web/entries/Source_Coding_Theorem.shtml`
The file was modified	`metadata/metadata` (diff)
The file was modified	`web/index.shtml` (diff)
The file was modified	`web/topics.shtml` (diff)