# HG changeset patch # User wenzelm # Date 1492798071 -7200 # Node ID 8369b33fda0a5418f1afc60bdd84e07b6dc69024 # Parent 6a00518bbfccf6709200c081d0035b367890eaac clarified session imports; diff -r 6a00518bbfcc -r 8369b33fda0a src/HOL/ROOT --- 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"