src/HOL/ROOT
changeset 66946 3d8fd98c7c86
parent 66932 149025fecca0
child 66950 1a5e90026391
     1.1 --- a/src/HOL/ROOT	Mon Oct 30 19:36:27 2017 +0100
     1.2 +++ b/src/HOL/ROOT	Mon Oct 30 20:04:10 2017 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    description {*
     1.5      HOL-Main with explicit proof terms.
     1.6    *}
     1.7 -  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     1.8 +  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     1.9    sessions
    1.10      "HOL-Library"
    1.11    theories
    1.12 @@ -177,7 +177,6 @@
    1.13      procedures. For documentation see "Hoare Logic for Mutual Recursion and
    1.14      Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
    1.15    *}
    1.16 -  options [document = false]
    1.17    theories EvenOdd
    1.18  
    1.19  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
    1.20 @@ -233,7 +232,7 @@
    1.21    document_files "root.bib" "root.tex"
    1.22  
    1.23  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
    1.24 -  options [document = false, browser_info = false]
    1.25 +  options [browser_info = false]
    1.26    sessions
    1.27      "HOL-Data_Structures"
    1.28      "HOL-ex"
    1.29 @@ -261,7 +260,6 @@
    1.30  
    1.31      Testing Metis and Sledgehammer.
    1.32    *}
    1.33 -  options [document = false]
    1.34    sessions
    1.35      "HOL-Decision_Procs"
    1.36    theories
    1.37 @@ -280,7 +278,6 @@
    1.38      Author:     Jasmin Blanchette, TU Muenchen
    1.39      Copyright   2009
    1.40    *}
    1.41 -  options [document = false]
    1.42    theories [quick_and_dirty] Nitpick_Examples
    1.43  
    1.44  session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
    1.45 @@ -384,12 +381,10 @@
    1.46    description {*
    1.47      Various decision procedures, typically involving reflection.
    1.48    *}
    1.49 -  options [document = false]
    1.50    theories
    1.51      Decision_Procs
    1.52  
    1.53  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    1.54 -  options [document = false]
    1.55    sessions
    1.56      "HOL-Isar_Examples"
    1.57    theories
    1.58 @@ -443,7 +438,6 @@
    1.59      including some minimal examples (in Test.thy) and a more typical example of
    1.60      a little functional language and its type system.
    1.61    *}
    1.62 -  options [document = false]
    1.63    theories Test Type
    1.64  
    1.65  session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
    1.66 @@ -505,7 +499,6 @@
    1.67      year=1995}
    1.68      ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    1.69    *}
    1.70 -  options [document = false]
    1.71    theories Solve
    1.72  
    1.73  session "HOL-Lattice" in Lattice = HOL +
    1.74 @@ -521,7 +514,6 @@
    1.75    description {*
    1.76      Miscellaneous examples for Higher-Order Logic.
    1.77    *}
    1.78 -  options [document = false]
    1.79    theories
    1.80      Adhoc_Overloading_Examples
    1.81      Antiquote
    1.82 @@ -667,19 +659,15 @@
    1.83    description {*
    1.84      Lamport's Temporal Logic of Actions.
    1.85    *}
    1.86 -  options [document = false]
    1.87    theories TLA
    1.88  
    1.89  session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
    1.90 -  options [document = false]
    1.91    theories Inc
    1.92  
    1.93  session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
    1.94 -  options [document = false]
    1.95    theories DBuffer
    1.96  
    1.97  session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
    1.98 -  options [document = false]
    1.99    theories MemoryImplementation
   1.100  
   1.101  session "HOL-TPTP" in TPTP = "HOL-Library" +
   1.102 @@ -690,7 +678,6 @@
   1.103  
   1.104      TPTP-related extensions.
   1.105    *}
   1.106 -  options [document = false]
   1.107    theories
   1.108      ATP_Theory_Export
   1.109      MaSh_Eval
   1.110 @@ -712,12 +699,10 @@
   1.111      Measure_Not_CCC
   1.112  
   1.113  session "HOL-Nominal" in Nominal = "HOL-Library" +
   1.114 -  options [document = false]
   1.115    theories
   1.116      Nominal
   1.117  
   1.118  session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   1.119 -  options [document = false]
   1.120    theories
   1.121      Class3
   1.122      CK_Machine
   1.123 @@ -758,7 +743,6 @@
   1.124    description {*
   1.125      (Co)datatype Examples.
   1.126    *}
   1.127 -  options [document = false]
   1.128    theories
   1.129      Compat
   1.130      Lambda_Term
   1.131 @@ -779,7 +763,6 @@
   1.132    description {*
   1.133      Corecursion Examples.
   1.134    *}
   1.135 -  options [document = false]
   1.136    theories
   1.137      LFilter
   1.138      Paper_Examples
   1.139 @@ -807,7 +790,6 @@
   1.140    document_files "root.bib" "root.tex"
   1.141  
   1.142  session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   1.143 -  options [document = false]
   1.144    theories WordExamples
   1.145  
   1.146  session "HOL-Statespace" in Statespace = HOL +
   1.147 @@ -824,20 +806,18 @@
   1.148    document_files "root.tex"
   1.149  
   1.150  session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   1.151 -  options [document = false]
   1.152    theories
   1.153      NSPrimes
   1.154  
   1.155  session "HOL-Mirabelle" in Mirabelle = HOL +
   1.156 -  options [document = false]
   1.157    theories Mirabelle_Test
   1.158  
   1.159  session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   1.160 -  options [document = false, timeout = 60]
   1.161 +  options [timeout = 60]
   1.162    theories Ex
   1.163  
   1.164  session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   1.165 -  options [document = false, quick_and_dirty]
   1.166 +  options [quick_and_dirty]
   1.167    theories
   1.168      Boogie
   1.169      SMT_Examples
   1.170 @@ -845,12 +825,11 @@
   1.171      SMT_Tests
   1.172  
   1.173  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   1.174 -  options [document = false]
   1.175    theories
   1.176      SPARK (global)
   1.177  
   1.178  session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   1.179 -  options [document = false, spark_prv = false]
   1.180 +  options [spark_prv = false]
   1.181    theories
   1.182      "Gcd/Greatest_Common_Divisor"
   1.183      "Liseq/Longest_Increasing_Subsequence"
   1.184 @@ -889,11 +868,9 @@
   1.185      "Simple_Gcd.ads"
   1.186  
   1.187  session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   1.188 -  options [document = false]
   1.189    theories MutabelleExtra
   1.190  
   1.191  session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   1.192 -  options [document = false]
   1.193    theories
   1.194      Quickcheck_Examples
   1.195      Quickcheck_Lattice_Examples
   1.196 @@ -908,7 +885,6 @@
   1.197    description {*
   1.198      Author:     Cezary Kaliszyk and Christian Urban
   1.199    *}
   1.200 -  options [document = false]
   1.201    theories
   1.202      DList
   1.203      Quotient_FSet
   1.204 @@ -923,7 +899,6 @@
   1.205      Lifting_Code_Dt_Test
   1.206  
   1.207  session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   1.208 -  options [document = false]
   1.209    theories
   1.210      Examples
   1.211      Predicate_Compile_Tests
   1.212 @@ -948,7 +923,6 @@
   1.213    description {*
   1.214      Experimental extension of Higher-Order Logic to allow translation of types to sets.
   1.215    *}
   1.216 -  options [document = false]
   1.217    theories
   1.218      Types_To_Sets
   1.219      "Examples/Prerequisites"
   1.220 @@ -974,7 +948,6 @@
   1.221    document_files "root.tex"
   1.222  
   1.223  session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   1.224 -  options [document = false]
   1.225    theories
   1.226      HOLCF_Library
   1.227      HOL_Cpo
   1.228 @@ -985,7 +958,6 @@
   1.229  
   1.230      This is the HOLCF-based denotational semantics of a simple WHILE-language.
   1.231    *}
   1.232 -  options [document = false]
   1.233    sessions
   1.234      "HOL-IMP"
   1.235    theories
   1.236 @@ -996,7 +968,6 @@
   1.237    description {*
   1.238      Miscellaneous examples for HOLCF.
   1.239    *}
   1.240 -  options [document = false]
   1.241    theories
   1.242      Dnat
   1.243      Dagstuhl
   1.244 @@ -1025,7 +996,6 @@
   1.245      "Specification and Development of Interactive Systems: Focus on Streams,
   1.246      Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
   1.247    *}
   1.248 -  options [document = false]
   1.249    theories
   1.250      Fstreams
   1.251      FOCUS
   1.252 @@ -1042,7 +1012,6 @@
   1.253      abstraction theory. Everything is based upon a domain-theoretic model of
   1.254      finite and infinite sequences.
   1.255    *}
   1.256 -  options [document = false]
   1.257    theories Abstraction
   1.258  
   1.259  session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   1.260 @@ -1051,7 +1020,6 @@
   1.261  
   1.262      The Alternating Bit Protocol performed in I/O-Automata.
   1.263    *}
   1.264 -  options [document = false]
   1.265    theories
   1.266      Correctness
   1.267      Spec
   1.268 @@ -1063,7 +1031,6 @@
   1.269      A network transmission protocol, performed in the
   1.270      I/O automata formalization by Olaf Mueller.
   1.271    *}
   1.272 -  options [document = false]
   1.273    theories Correctness
   1.274  
   1.275  session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   1.276 @@ -1072,14 +1039,12 @@
   1.277  
   1.278      Memory storage case study.
   1.279    *}
   1.280 -  options [document = false]
   1.281    theories Correctness
   1.282  
   1.283  session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   1.284    description {*
   1.285      Author:     Olaf Mueller
   1.286    *}
   1.287 -  options [document = false]
   1.288    theories
   1.289      TrivEx
   1.290      TrivEx2