--- a/src/HOL/ROOT Mon Oct 02 16:08:43 2017 +0200
+++ b/src/HOL/ROOT Mon Oct 02 16:41:59 2017 +0200
@@ -409,7 +409,6 @@
*}
options [parallel_proofs = 0, quick_and_dirty = false]
sessions
- "HOL-Library"
"HOL-Computational_Algebra"
theories
Greatest_Common_Divisor
@@ -524,13 +523,11 @@
theories CompleteLattice
document_files "root.tex"
-session "HOL-ex" (timing) in ex = "HOL-Library" +
+session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
description {*
Miscellaneous examples for Higher-Order Logic.
*}
options [document = false]
- sessions
- "HOL-Number_Theory"
theories
Adhoc_Overloading_Examples
Antiquote
@@ -719,10 +716,8 @@
Koepf_Duermuth_Countermeasure
Measure_Not_CCC
-session "HOL-Nominal" in Nominal = HOL +
+session "HOL-Nominal" in Nominal = "HOL-Library" +
options [document = false]
- sessions
- "HOL-Library"
theories
Nominal
@@ -1022,15 +1017,13 @@
"Examples/Finite"
"Examples/T2_Spaces"
-session HOLCF (main timing) in HOLCF = HOL +
+session HOLCF (main timing) in HOLCF = "HOL-Library" +
description {*
Author: Franz Regensburger
Author: Brian Huffman
HOLCF -- a semantic extension of HOL by the LCF logic.
*}
- sessions
- "HOL-Library"
theories
HOLCF (global)
document_files "root.tex"