eliminated old-style no-document imports;
authorwenzelm
Mon Oct 02 16:08:43 2017 +0200 (20 months ago)
changeset 667511f92f5cc70e4
parent 66750 41fbe4a3aac9
child 66752 1dd5633f5862
eliminated old-style no-document imports;
src/Doc/ROOT
src/HOL/ROOT
     1.1 --- a/src/Doc/ROOT	Mon Oct 02 15:51:52 2017 +0200
     1.2 +++ b/src/Doc/ROOT	Mon Oct 02 16:08:43 2017 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4    options [document_variants = "corec"]
     1.5    sessions
     1.6      Datatypes
     1.7 -  theories [document = false] Datatypes.Setup
     1.8    theories Corec
     1.9    document_files (in "..")
    1.10      "prepare_document"
    1.11 @@ -248,9 +247,6 @@
    1.12    options [document_variants = "sugar"]
    1.13    sessions
    1.14      "HOL-Library"
    1.15 -  theories [document = false]
    1.16 -    "HOL-Library.LaTeXsugar"
    1.17 -    "HOL-Library.OptionalSugar"
    1.18    theories Sugar
    1.19    document_files (in "..")
    1.20      "prepare_document"
     2.1 --- a/src/HOL/ROOT	Mon Oct 02 15:51:52 2017 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Oct 02 16:08:43 2017 +0200
     2.3 @@ -121,8 +121,6 @@
     2.4      Exp demonstrates the use of iterated inductive definitions to reason about
     2.5      mutually recursive relations.
     2.6    *}
     2.7 -  theories [document = false]
     2.8 -    "HOL-Library.Old_Datatype"
     2.9    theories [quick_and_dirty]
    2.10      Common_Patterns
    2.11    theories
    2.12 @@ -142,12 +140,6 @@
    2.13  
    2.14  session "HOL-IMP" (timing) in IMP = "HOL-Library" +
    2.15    options [document_variants = document]
    2.16 -  theories [document = false]
    2.17 -    "HOL-Library.While_Combinator"
    2.18 -    "HOL-Library.Char_ord"
    2.19 -    "HOL-Library.List_lexord"
    2.20 -    "HOL-Library.Quotient_List"
    2.21 -    "HOL-Library.Extended"
    2.22    theories
    2.23      BExp
    2.24      ASM
    2.25 @@ -200,8 +192,6 @@
    2.26      "HOL-Number_Theory"
    2.27    theories [document = false]
    2.28      Less_False
    2.29 -    "HOL-Library.Multiset"
    2.30 -    "HOL-Number_Theory.Fib"
    2.31    theories
    2.32      Sorting
    2.33      Balance
    2.34 @@ -227,11 +217,6 @@
    2.35    *}
    2.36    sessions
    2.37      "HOL-Algebra"
    2.38 -  theories [document = false]
    2.39 -    "HOL-Library.FuncSet"
    2.40 -    "HOL-Library.Multiset"
    2.41 -    "HOL-Algebra.Ring"
    2.42 -    "HOL-Algebra.FiniteProduct"
    2.43    theories
    2.44      Number_Theory
    2.45    document_files
    2.46 @@ -310,11 +295,6 @@
    2.47  
    2.48      The Isabelle Algebraic Library.
    2.49    *}
    2.50 -  theories [document = false]
    2.51 -    (* Preliminaries from set and number theory *)
    2.52 -    "HOL-Library.FuncSet"
    2.53 -    "HOL-Computational_Algebra.Primes"
    2.54 -    "HOL-Library.Permutation"
    2.55    theories
    2.56      (* Orders and Lattices *)
    2.57      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
    2.58 @@ -403,10 +383,6 @@
    2.59  
    2.60  session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
    2.61    options [print_mode = "iff,no_brackets"]
    2.62 -  theories [document = false]
    2.63 -    "HOL-Library.Countable"
    2.64 -    "HOL-Library.Monad_Syntax"
    2.65 -    "HOL-Library.LaTeXsugar"
    2.66    theories Imperative_HOL_ex
    2.67    document_files "root.bib" "root.tex"
    2.68  
    2.69 @@ -435,11 +411,6 @@
    2.70    sessions
    2.71      "HOL-Library"
    2.72      "HOL-Computational_Algebra"
    2.73 -  theories [document = false]
    2.74 -    "HOL-Library.Code_Target_Numeral"
    2.75 -    "HOL-Library.Monad_Syntax"
    2.76 -    "HOL-Computational_Algebra.Primes"
    2.77 -    "HOL-Library.Open_State_Syntax"
    2.78    theories
    2.79      Greatest_Common_Divisor
    2.80      Warshall
    2.81 @@ -490,8 +461,6 @@
    2.82    *}
    2.83    sessions
    2.84      "HOL-Eisbach"
    2.85 -  theories [document = false]
    2.86 -    "HOL-Library.While_Combinator"
    2.87    theories
    2.88      MicroJava
    2.89    document_files
    2.90 @@ -653,9 +622,6 @@
    2.91      Miscellaneous Isabelle/Isar examples.
    2.92    *}
    2.93    options [quick_and_dirty]
    2.94 -  theories [document = false]
    2.95 -    "HOL-Library.Lattice_Syntax"
    2.96 -    "HOL-Computational_Algebra.Primes"
    2.97    theories
    2.98      Knaster_Tarski
    2.99      Peirce
   2.100 @@ -694,8 +660,6 @@
   2.101    description {*
   2.102      Verification of the SET Protocol.
   2.103    *}
   2.104 -  theories [document = false]
   2.105 -    "HOL-Library.Nat_Bijection"
   2.106    theories
   2.107      SET_Protocol
   2.108    document_files "root.tex"
   2.109 @@ -745,12 +709,6 @@
   2.110      ATP_Problem_Import
   2.111  
   2.112  session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   2.113 -  theories [document = false]
   2.114 -    "HOL-Library.Countable"
   2.115 -    "HOL-Library.Permutation"
   2.116 -    "HOL-Library.Order_Continuity"
   2.117 -    "HOL-Library.Diagonal_Subsequence"
   2.118 -    "HOL-Library.Finite_Map"
   2.119    theories
   2.120      Probability (global)
   2.121    document_files "root.tex"
   2.122 @@ -1073,9 +1031,6 @@
   2.123    *}
   2.124    sessions
   2.125      "HOL-Library"
   2.126 -  theories [document = false]
   2.127 -    "HOL-Library.Nat_Bijection"
   2.128 -    "HOL-Library.Countable"
   2.129    theories
   2.130      HOLCF (global)
   2.131    document_files "root.tex"