# HG changeset patch # User wenzelm # Date 1493027571 -7200 # Node ID 0f3fdf689bf9f55fe4e5efeb406a10c70a67f3d4 # Parent 6acb28e5ba4176c163dd6956e4388bb065d99716 clarified parent session images, to avoid duplicate loading of theories; diff -r 6acb28e5ba41 -r 0f3fdf689bf9 src/Benchmarks/ROOT --- a/src/Benchmarks/ROOT Mon Apr 24 11:23:07 2017 +0200 +++ b/src/Benchmarks/ROOT Mon Apr 24 11:52:51 2017 +0200 @@ -1,6 +1,6 @@ chapter HOL -session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL + +session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" + description {* Big (co)datatypes. *} @@ -10,7 +10,7 @@ IsaFoR Misc_N2M -session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL + +session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = "HOL-Library" + theories [quick_and_dirty] Find_Unused_Assms_Examples Needham_Schroeder_No_Attacker_Example diff -r 6acb28e5ba41 -r 0f3fdf689bf9 src/Doc/ROOT --- a/src/Doc/ROOT Mon Apr 24 11:23:07 2017 +0200 +++ b/src/Doc/ROOT Mon Apr 24 11:52:51 2017 +0200 @@ -46,6 +46,8 @@ session Corec (doc) in "Corec" = "HOL-Library" + options [document_variants = "corec"] + sessions + Datatypes theories [document = false] "../Datatypes/Setup" theories Corec document_files (in "..") @@ -170,7 +172,7 @@ "root.tex" "style.sty" -session Isar_Ref (doc) in "Isar_Ref" = HOL + +session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" + options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] theories Preface @@ -244,7 +246,9 @@ session Sugar (doc) in "Sugar" = HOL + options [document_variants = "sugar"] - theories [document = ""] + sessions + "HOL-Library" + theories [document = false] "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" theories Sugar @@ -436,7 +440,7 @@ theories "Protocol/NS_Public" "Documents/Documents" - theories [document = ""] + theories [document = false] "Types/Setup" theories [thy_output_margin = 64, thy_output_indent = 0] "Types/Numbers" @@ -502,7 +506,7 @@ "root.tex" "style.sty" -session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" + +session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" + options [document = false] theories Setup diff -r 6acb28e5ba41 -r 0f3fdf689bf9 src/HOL/ROOT --- a/src/HOL/ROOT Mon Apr 24 11:23:07 2017 +0200 +++ b/src/HOL/ROOT Mon Apr 24 11:52:51 2017 +0200 @@ -96,6 +96,8 @@ subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. *} + sessions + "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" @@ -136,7 +138,7 @@ Com document_files "root.tex" -session "HOL-IMP" (timing) in IMP = HOL + +session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories [document = false] "~~/src/HOL/Library/While_Combinator" @@ -192,6 +194,8 @@ session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] + sessions + "HOL-Number_Theory" theories [document = false] Less_False "~~/src/HOL/Library/Multiset" @@ -248,6 +252,9 @@ session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" + options [document = false, browser_info = false] + sessions + "HOL-Data_Structures" + "HOL-ex" theories Generate Generate_Binary_Nat @@ -265,7 +272,7 @@ theories [condition = "ISABELLE_SMLNJ"] Code_Test_SMLNJ -session "HOL-Metis_Examples" (timing) in Metis_Examples = HOL + +session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen @@ -273,6 +280,8 @@ Testing Metis and Sledgehammer. *} options [document = false] + sessions + "HOL-Decision_Procs" theories Abstraction Big_O @@ -284,7 +293,7 @@ Trans_Closure Sets -session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + +session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" + description {* Author: Jasmin Blanchette, TU Muenchen Copyright 2009 @@ -332,7 +341,7 @@ More_Ring document_files "root.bib" "root.tex" -session "HOL-Auth" (timing) in Auth = HOL + +session "HOL-Auth" (timing) in Auth = "HOL-Library" + description {* A new approach to verifying authentication protocols. *} @@ -388,13 +397,15 @@ ELT document_files "root.tex" -session "HOL-Unix" in Unix = HOL + +session "HOL-Unix" in Unix = "HOL-Library" + options [print_mode = "no_brackets,no_type_brackets"] theories Unix document_files "root.bib" "root.tex" -session "HOL-ZF" in ZF = HOL + - theories MainZF Games +session "HOL-ZF" in ZF = "HOL-Library" + + theories + MainZF + Games document_files "root.tex" session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" + @@ -416,6 +427,8 @@ session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + options [document = false] + sessions + "HOL-Isar_Examples" theories Hilbert_Classical Proof_Terms @@ -482,6 +495,8 @@ machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. *} + sessions + "HOL-Eisbach" theories [document = false] "~~/src/HOL/Library/While_Combinator" theories @@ -498,7 +513,7 @@ theories Example document_files "root.bib" "root.tex" -session "HOL-Bali" (timing) in Bali = HOL + +session "HOL-Bali" (timing) in Bali = "HOL-Library" + theories AxExample AxSound @@ -716,7 +731,7 @@ options [document = false] theories MemoryImplementation -session "HOL-TPTP" in TPTP = HOL + +session "HOL-TPTP" in TPTP = "HOL-Library" + description {* Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge @@ -753,7 +768,10 @@ session "HOL-Nominal" in Nominal = HOL + options [document = false] - theories Nominal + sessions + "HOL-Library" + theories + Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + options [document = false] @@ -781,7 +799,7 @@ theories [quick_and_dirty] VC_Condition -session "HOL-Cardinals" (timing) in Cardinals = HOL + +session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" + description {* Ordinals and Cardinals, Full Theories. *} @@ -799,6 +817,8 @@ (Co)datatype Examples. *} options [document = false] + sessions + "HOL-Library" theories Compat Lambda_Term @@ -815,7 +835,7 @@ Misc_Primcorec Misc_Primrec -session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL + +session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description {* Corecursion Examples. *} @@ -838,6 +858,8 @@ "Tests/Type_Class" session "HOL-Word" (main timing) in Word = HOL + + sessions + "HOL-Library" theories Word document_files "root.bib" "root.tex" @@ -944,7 +966,7 @@ "RIPEMD-160/rmd/s_r.rls" "RIPEMD-160/rmd/s_r.siv" -session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + +session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK-Examples" + options [show_question_marks = false, spark_prv = false] theories Example_Verification @@ -978,7 +1000,7 @@ "Simple_Gcd.adb" "Simple_Gcd.ads" -session "HOL-Mutabelle" in Mutabelle = HOL + +session "HOL-Mutabelle" in Mutabelle = "HOL-Library" + options [document = false] theories MutabelleExtra @@ -1081,10 +1103,13 @@ This is the HOLCF-based denotational semantics of a simple WHILE-language. *} options [document = false] - theories HoareEx + sessions + "HOL-IMP" + theories + HoareEx document_files "root.tex" -session "HOLCF-ex" in "HOLCF/ex" = HOLCF + +session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description {* Miscellaneous examples for HOLCF. *} @@ -1102,7 +1127,7 @@ Letrec Pattern_Match -session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF + +session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description {* FOCUS: a theory of stream-processing functions Isabelle/HOLCF.