--- a/src/HOL/ROOT Fri Apr 21 19:43:53 2017 +0200
+++ b/src/HOL/ROOT Fri Apr 21 20:07:51 2017 +0200
@@ -20,7 +20,8 @@
*}
options [document = false, theory_qualifier = "HOL",
quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
- sessions "HOL-Library"
+ sessions
+ "HOL-Library"
theories
GCD
Binomial
@@ -63,6 +64,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
@@ -74,6 +78,8 @@
Circle_Area
session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL +
+ sessions
+ "HOL-Library"
theories
Computational_Algebra
(*conflicting type class instantiations and dependent applications*)
@@ -98,7 +104,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 +
@@ -118,6 +127,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]
@@ -219,6 +230,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"
@@ -247,6 +262,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
@@ -307,6 +325,9 @@
The Isabelle Algebraic Library.
*}
+ sessions
+ "HOL-Library"
+ "HOL-Computational_Algebra"
theories [document = false]
(* Preliminaries from set and number theory *)
"~~/src/HOL/Library/FuncSet"
@@ -398,6 +419,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"
@@ -410,7 +433,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]
@@ -424,6 +451,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"
@@ -449,7 +479,8 @@
*}
options [print_mode = "no_brackets",
parallel_proofs = 0, quick_and_dirty = false]
- sessions "HOL-Library"
+ sessions
+ "HOL-Library"
theories
Eta
StrongNorm
@@ -476,6 +507,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
@@ -545,6 +578,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
@@ -641,6 +677,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"
@@ -680,8 +719,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 +
@@ -729,6 +772,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"
@@ -855,7 +900,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]
@@ -992,6 +1040,8 @@
Author: Cezary Kaliszyk and Christian Urban
*}
options [document = false]
+ sessions
+ "HOL-Library"
theories
DList
Quotient_FSet
@@ -1045,6 +1095,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"