# HG changeset patch # User wenzelm # Date 1506955319 -7200 # Node ID 1dd5633f58629a761216e3ecf468fa106c9236a3 # Parent 1f92f5cc70e40b7d21fa0475789d2331613fb972 clarified imports: prefer parent session images; diff -r 1f92f5cc70e4 -r 1dd5633f5862 src/HOL/ROOT --- 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"