--- 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
--- 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
--- 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.