src/HOL/ROOT
changeset 65544 c09c11386ca5
parent 65515 f595b7532dc9
parent 65543 8369b33fda0a
child 65548 b7caa2b8bdbf
--- a/src/HOL/ROOT	Thu Apr 20 16:21:29 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 20:36:20 2017 +0200
@@ -20,8 +20,12 @@
   *}
   options [document = false, theory_qualifier = "HOL",
     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
-  sessions "HOL-Library"
-  theories "HOL-Library.Old_Datatype"
+  sessions
+    "HOL-Library"
+  theories
+    GCD
+    Binomial
+    "HOL-Library.Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
@@ -59,6 +63,9 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories
     Analysis
   document_files
@@ -70,6 +77,8 @@
     Circle_Area
 
 session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL +
+  sessions
+    "HOL-Library"
   theories
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
@@ -94,7 +103,10 @@
     subspaces (not only one-dimensional subspaces), can be extended to a
     continous linearform on the whole vectorspace.
   *}
-  theories Hahn_Banach
+  sessions
+    "HOL-Library"
+  theories
+    Hahn_Banach
   document_files "root.bib" "root.tex"
 
 session "HOL-Induct" in Induct = HOL +
@@ -114,6 +126,8 @@
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Old_Datatype"
   theories [quick_and_dirty]
@@ -190,7 +204,7 @@
 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   theories [document = false]
-    "Less_False"
+    Less_False
     "~~/src/HOL/Library/Multiset"
     "~~/src/HOL/Number_Theory/Fib"
   theories
@@ -215,6 +229,10 @@
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Algebra"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/FuncSet"
     "~~/src/HOL/Library/Multiset"
@@ -243,6 +261,9 @@
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, browser_info = false]
+  sessions
+    "HOL-Computational_Algebra"
+    "HOL-Number_Theory"
   theories
     Generate
     Generate_Binary_Nat
@@ -303,6 +324,9 @@
 
     The Isabelle Algebraic Library.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     (* Preliminaries from set and number theory *)
     "~~/src/HOL/Library/FuncSet"
@@ -348,7 +372,7 @@
   *}
   theories
     (*Basic meta-theory*)
-    "UNITY_Main"
+    UNITY_Main
 
     (*Simple examples: no composition*)
     "Simple/Deadlock"
@@ -380,7 +404,7 @@
     "Comp/Client"
 
     (*obsolete*)
-    "ELT"
+    ELT
   document_files "root.tex"
 
 session "HOL-Unix" in Unix = HOL +
@@ -394,6 +418,8 @@
 
 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   options [print_mode = "iff,no_brackets"]
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -406,7 +432,11 @@
     Various decision procedures, typically involving reflection.
   *}
   options [document = false]
-  theories Decision_Procs
+  sessions
+    "HOL-Library"
+    "HOL-Algebra"
+  theories
+    Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   options [document = false]
@@ -420,6 +450,9 @@
     Examples for program extraction in Higher-Order Logic.
   *}
   options [parallel_proofs = 0, quick_and_dirty = false]
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -445,8 +478,8 @@
   *}
   options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
-  theories [document = false]
-    "~~/src/HOL/Library/Code_Target_Int"
+  sessions
+    "HOL-Library"
   theories
     Eta
     StrongNorm
@@ -473,6 +506,8 @@
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/While_Combinator"
   theories
@@ -542,6 +577,9 @@
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Number_Theory"
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
@@ -638,6 +676,9 @@
     Miscellaneous Isabelle/Isar examples.
   *}
   options [quick_and_dirty]
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Computational_Algebra/Primes"
@@ -677,8 +718,12 @@
   description {*
     Verification of the SET Protocol.
   *}
-  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
-  theories SET_Protocol
+  sessions
+    "HOL-Library"
+  theories [document = false]
+    "~~/src/HOL/Library/Nat_Bijection"
+  theories
+    SET_Protocol
   document_files "root.tex"
 
 session "HOL-Matrix_LP" in Matrix_LP = HOL +
@@ -726,6 +771,8 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
@@ -738,9 +785,9 @@
 
 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   theories
-    "Dining_Cryptographers"
-    "Koepf_Duermuth_Countermeasure"
-    "Measure_Not_CCC"
+    Dining_Cryptographers
+    Koepf_Duermuth_Countermeasure
+    Measure_Not_CCC
 
 session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
@@ -852,7 +899,10 @@
 
 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   options [document = false]
-  theories NSPrimes
+  sessions
+    "HOL-Computational_Algebra"
+  theories
+    NSPrimes
 
 session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]
@@ -989,6 +1039,8 @@
     Author:     Cezary Kaliszyk and Christian Urban
   *}
   options [document = false]
+  sessions
+    "HOL-Library"
   theories
     DList
     Quotient_FSet
@@ -1042,6 +1094,8 @@
 
     HOLCF -- a semantic extension of HOL by the LCF logic.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Nat_Bijection"
     "~~/src/HOL/Library/Countable"
@@ -1121,7 +1175,7 @@
     finite and infinite sequences.
   *}
   options [document = false]
-  theories "Abstraction"
+  theories Abstraction
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description {*