ROOT cleanup: empty 'document_files' means there is no document;
authorwenzelm
Mon Oct 30 20:04:10 2017 +0100 (19 months ago)
changeset 669463d8fd98c7c86
parent 66945 b6f787a17fbe
child 66947 eefbb2300669
ROOT cleanup: empty 'document_files' means there is no document;
src/Benchmarks/ROOT
src/CCL/ROOT
src/Cube/ROOT
src/Doc/ROOT
src/FOLP/ROOT
src/HOL/ROOT
src/LCF/ROOT
src/Sequents/ROOT
src/ZF/ROOT
     1.1 --- a/src/Benchmarks/ROOT	Mon Oct 30 19:36:27 2017 +0100
     1.2 +++ b/src/Benchmarks/ROOT	Mon Oct 30 20:04:10 2017 +0100
     1.3 @@ -4,7 +4,6 @@
     1.4    description {*
     1.5      Big (co)datatypes.
     1.6    *}
     1.7 -  options [document = false]
     1.8    theories
     1.9      Brackin
    1.10      IsaFoR
    1.11 @@ -21,6 +20,5 @@
    1.12    description {*
    1.13      Big records.
    1.14    *}
    1.15 -  options [document = false]
    1.16    theories
    1.17      Record_Benchmark
     2.1 --- a/src/CCL/ROOT	Mon Oct 30 19:36:27 2017 +0100
     2.2 +++ b/src/CCL/ROOT	Mon Oct 30 20:04:10 2017 +0100
     2.3 @@ -10,7 +10,6 @@
     2.4      A computational logic for an untyped functional language with
     2.5      evaluation to weak head-normal form.
     2.6    *}
     2.7 -  options [document = false]
     2.8    sessions
     2.9      FOL
    2.10    theories
    2.11 @@ -22,4 +21,3 @@
    2.12      "ex/List"
    2.13      "ex/Stream"
    2.14      "ex/Flag"
    2.15 -
     3.1 --- a/src/Cube/ROOT	Mon Oct 30 19:36:27 2017 +0100
     3.2 +++ b/src/Cube/ROOT	Mon Oct 30 20:04:10 2017 +0100
     3.3 @@ -13,6 +13,4 @@
     3.4      For more information about the Lambda-Cube, see H. Barendregt, Introduction
     3.5      to Generalised Type Systems, J. Functional Programming.
     3.6    *}
     3.7 -  options [document = false]
     3.8    theories Example
     3.9 -
     4.1 --- a/src/Doc/ROOT	Mon Oct 30 19:36:27 2017 +0100
     4.2 +++ b/src/Doc/ROOT	Mon Oct 30 20:04:10 2017 +0100
     4.3 @@ -17,7 +17,6 @@
     4.4      "style.sty"
     4.5  
     4.6  session Codegen_Basics in "Codegen" = "HOL-Library" +
     4.7 -  options [document = false]
     4.8    theories
     4.9      Setup
    4.10  
    4.11 @@ -505,6 +504,5 @@
    4.12      "style.sty"
    4.13  
    4.14  session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
    4.15 -  options [document = false]
    4.16    theories
    4.17      Setup
     5.1 --- a/src/FOLP/ROOT	Mon Oct 30 19:36:27 2017 +0100
     5.2 +++ b/src/FOLP/ROOT	Mon Oct 30 20:04:10 2017 +0100
     5.3 @@ -9,7 +9,6 @@
     5.4  
     5.5      Presence of unknown proof term means that matching does not behave as expected.
     5.6    *}
     5.7 -  options [document = false]
     5.8    theories
     5.9      IFOLP (global)
    5.10      FOLP (global)
    5.11 @@ -21,7 +20,6 @@
    5.12  
    5.13      Examples for First-Order Logic.
    5.14    *}
    5.15 -  options [document = false]
    5.16    theories
    5.17      Intro
    5.18      Nat
    5.19 @@ -33,4 +31,3 @@
    5.20      Quantifiers_Int
    5.21      Propositional_Cla
    5.22      Quantifiers_Cla
    5.23 -
     6.1 --- a/src/HOL/ROOT	Mon Oct 30 19:36:27 2017 +0100
     6.2 +++ b/src/HOL/ROOT	Mon Oct 30 20:04:10 2017 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4    description {*
     6.5      HOL-Main with explicit proof terms.
     6.6    *}
     6.7 -  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     6.8 +  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     6.9    sessions
    6.10      "HOL-Library"
    6.11    theories
    6.12 @@ -177,7 +177,6 @@
    6.13      procedures. For documentation see "Hoare Logic for Mutual Recursion and
    6.14      Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
    6.15    *}
    6.16 -  options [document = false]
    6.17    theories EvenOdd
    6.18  
    6.19  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
    6.20 @@ -233,7 +232,7 @@
    6.21    document_files "root.bib" "root.tex"
    6.22  
    6.23  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
    6.24 -  options [document = false, browser_info = false]
    6.25 +  options [browser_info = false]
    6.26    sessions
    6.27      "HOL-Data_Structures"
    6.28      "HOL-ex"
    6.29 @@ -261,7 +260,6 @@
    6.30  
    6.31      Testing Metis and Sledgehammer.
    6.32    *}
    6.33 -  options [document = false]
    6.34    sessions
    6.35      "HOL-Decision_Procs"
    6.36    theories
    6.37 @@ -280,7 +278,6 @@
    6.38      Author:     Jasmin Blanchette, TU Muenchen
    6.39      Copyright   2009
    6.40    *}
    6.41 -  options [document = false]
    6.42    theories [quick_and_dirty] Nitpick_Examples
    6.43  
    6.44  session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
    6.45 @@ -384,12 +381,10 @@
    6.46    description {*
    6.47      Various decision procedures, typically involving reflection.
    6.48    *}
    6.49 -  options [document = false]
    6.50    theories
    6.51      Decision_Procs
    6.52  
    6.53  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    6.54 -  options [document = false]
    6.55    sessions
    6.56      "HOL-Isar_Examples"
    6.57    theories
    6.58 @@ -443,7 +438,6 @@
    6.59      including some minimal examples (in Test.thy) and a more typical example of
    6.60      a little functional language and its type system.
    6.61    *}
    6.62 -  options [document = false]
    6.63    theories Test Type
    6.64  
    6.65  session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
    6.66 @@ -505,7 +499,6 @@
    6.67      year=1995}
    6.68      ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    6.69    *}
    6.70 -  options [document = false]
    6.71    theories Solve
    6.72  
    6.73  session "HOL-Lattice" in Lattice = HOL +
    6.74 @@ -521,7 +514,6 @@
    6.75    description {*
    6.76      Miscellaneous examples for Higher-Order Logic.
    6.77    *}
    6.78 -  options [document = false]
    6.79    theories
    6.80      Adhoc_Overloading_Examples
    6.81      Antiquote
    6.82 @@ -667,19 +659,15 @@
    6.83    description {*
    6.84      Lamport's Temporal Logic of Actions.
    6.85    *}
    6.86 -  options [document = false]
    6.87    theories TLA
    6.88  
    6.89  session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
    6.90 -  options [document = false]
    6.91    theories Inc
    6.92  
    6.93  session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
    6.94 -  options [document = false]
    6.95    theories DBuffer
    6.96  
    6.97  session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
    6.98 -  options [document = false]
    6.99    theories MemoryImplementation
   6.100  
   6.101  session "HOL-TPTP" in TPTP = "HOL-Library" +
   6.102 @@ -690,7 +678,6 @@
   6.103  
   6.104      TPTP-related extensions.
   6.105    *}
   6.106 -  options [document = false]
   6.107    theories
   6.108      ATP_Theory_Export
   6.109      MaSh_Eval
   6.110 @@ -712,12 +699,10 @@
   6.111      Measure_Not_CCC
   6.112  
   6.113  session "HOL-Nominal" in Nominal = "HOL-Library" +
   6.114 -  options [document = false]
   6.115    theories
   6.116      Nominal
   6.117  
   6.118  session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   6.119 -  options [document = false]
   6.120    theories
   6.121      Class3
   6.122      CK_Machine
   6.123 @@ -758,7 +743,6 @@
   6.124    description {*
   6.125      (Co)datatype Examples.
   6.126    *}
   6.127 -  options [document = false]
   6.128    theories
   6.129      Compat
   6.130      Lambda_Term
   6.131 @@ -779,7 +763,6 @@
   6.132    description {*
   6.133      Corecursion Examples.
   6.134    *}
   6.135 -  options [document = false]
   6.136    theories
   6.137      LFilter
   6.138      Paper_Examples
   6.139 @@ -807,7 +790,6 @@
   6.140    document_files "root.bib" "root.tex"
   6.141  
   6.142  session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   6.143 -  options [document = false]
   6.144    theories WordExamples
   6.145  
   6.146  session "HOL-Statespace" in Statespace = HOL +
   6.147 @@ -824,20 +806,18 @@
   6.148    document_files "root.tex"
   6.149  
   6.150  session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   6.151 -  options [document = false]
   6.152    theories
   6.153      NSPrimes
   6.154  
   6.155  session "HOL-Mirabelle" in Mirabelle = HOL +
   6.156 -  options [document = false]
   6.157    theories Mirabelle_Test
   6.158  
   6.159  session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   6.160 -  options [document = false, timeout = 60]
   6.161 +  options [timeout = 60]
   6.162    theories Ex
   6.163  
   6.164  session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   6.165 -  options [document = false, quick_and_dirty]
   6.166 +  options [quick_and_dirty]
   6.167    theories
   6.168      Boogie
   6.169      SMT_Examples
   6.170 @@ -845,12 +825,11 @@
   6.171      SMT_Tests
   6.172  
   6.173  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   6.174 -  options [document = false]
   6.175    theories
   6.176      SPARK (global)
   6.177  
   6.178  session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   6.179 -  options [document = false, spark_prv = false]
   6.180 +  options [spark_prv = false]
   6.181    theories
   6.182      "Gcd/Greatest_Common_Divisor"
   6.183      "Liseq/Longest_Increasing_Subsequence"
   6.184 @@ -889,11 +868,9 @@
   6.185      "Simple_Gcd.ads"
   6.186  
   6.187  session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   6.188 -  options [document = false]
   6.189    theories MutabelleExtra
   6.190  
   6.191  session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   6.192 -  options [document = false]
   6.193    theories
   6.194      Quickcheck_Examples
   6.195      Quickcheck_Lattice_Examples
   6.196 @@ -908,7 +885,6 @@
   6.197    description {*
   6.198      Author:     Cezary Kaliszyk and Christian Urban
   6.199    *}
   6.200 -  options [document = false]
   6.201    theories
   6.202      DList
   6.203      Quotient_FSet
   6.204 @@ -923,7 +899,6 @@
   6.205      Lifting_Code_Dt_Test
   6.206  
   6.207  session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   6.208 -  options [document = false]
   6.209    theories
   6.210      Examples
   6.211      Predicate_Compile_Tests
   6.212 @@ -948,7 +923,6 @@
   6.213    description {*
   6.214      Experimental extension of Higher-Order Logic to allow translation of types to sets.
   6.215    *}
   6.216 -  options [document = false]
   6.217    theories
   6.218      Types_To_Sets
   6.219      "Examples/Prerequisites"
   6.220 @@ -974,7 +948,6 @@
   6.221    document_files "root.tex"
   6.222  
   6.223  session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   6.224 -  options [document = false]
   6.225    theories
   6.226      HOLCF_Library
   6.227      HOL_Cpo
   6.228 @@ -985,7 +958,6 @@
   6.229  
   6.230      This is the HOLCF-based denotational semantics of a simple WHILE-language.
   6.231    *}
   6.232 -  options [document = false]
   6.233    sessions
   6.234      "HOL-IMP"
   6.235    theories
   6.236 @@ -996,7 +968,6 @@
   6.237    description {*
   6.238      Miscellaneous examples for HOLCF.
   6.239    *}
   6.240 -  options [document = false]
   6.241    theories
   6.242      Dnat
   6.243      Dagstuhl
   6.244 @@ -1025,7 +996,6 @@
   6.245      "Specification and Development of Interactive Systems: Focus on Streams,
   6.246      Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
   6.247    *}
   6.248 -  options [document = false]
   6.249    theories
   6.250      Fstreams
   6.251      FOCUS
   6.252 @@ -1042,7 +1012,6 @@
   6.253      abstraction theory. Everything is based upon a domain-theoretic model of
   6.254      finite and infinite sequences.
   6.255    *}
   6.256 -  options [document = false]
   6.257    theories Abstraction
   6.258  
   6.259  session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   6.260 @@ -1051,7 +1020,6 @@
   6.261  
   6.262      The Alternating Bit Protocol performed in I/O-Automata.
   6.263    *}
   6.264 -  options [document = false]
   6.265    theories
   6.266      Correctness
   6.267      Spec
   6.268 @@ -1063,7 +1031,6 @@
   6.269      A network transmission protocol, performed in the
   6.270      I/O automata formalization by Olaf Mueller.
   6.271    *}
   6.272 -  options [document = false]
   6.273    theories Correctness
   6.274  
   6.275  session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   6.276 @@ -1072,14 +1039,12 @@
   6.277  
   6.278      Memory storage case study.
   6.279    *}
   6.280 -  options [document = false]
   6.281    theories Correctness
   6.282  
   6.283  session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   6.284    description {*
   6.285      Author:     Olaf Mueller
   6.286    *}
   6.287 -  options [document = false]
   6.288    theories
   6.289      TrivEx
   6.290      TrivEx2
     7.1 --- a/src/LCF/ROOT	Mon Oct 30 19:36:27 2017 +0100
     7.2 +++ b/src/LCF/ROOT	Mon Oct 30 20:04:10 2017 +0100
     7.3 @@ -10,7 +10,6 @@
     7.4      Useful references on LCF: Lawrence C. Paulson,
     7.5      Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
     7.6    *}
     7.7 -  options [document = false]
     7.8    sessions
     7.9      FOL
    7.10    theories
    7.11 @@ -21,4 +20,3 @@
    7.12      "ex/Ex2"
    7.13      "ex/Ex3"
    7.14      "ex/Ex4"
    7.15 -
     8.1 --- a/src/Sequents/ROOT	Mon Oct 30 19:36:27 2017 +0100
     8.2 +++ b/src/Sequents/ROOT	Mon Oct 30 20:04:10 2017 +0100
     8.3 @@ -37,7 +37,6 @@
     8.4      S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
     8.5      of Cambridge Computer Lab, 1995, ed L. Paulson)
     8.6    *}
     8.7 -  options [document = false]
     8.8    theories
     8.9      LK
    8.10      ILL
    8.11 @@ -53,4 +52,3 @@
    8.12      "LK/Quantifiers"
    8.13      "LK/Hard_Quantifiers"
    8.14      "LK/Nat"
    8.15 -
     9.1 --- a/src/ZF/ROOT	Mon Oct 30 19:36:27 2017 +0100
     9.2 +++ b/src/ZF/ROOT	Mon Oct 30 20:04:10 2017 +0100
     9.3 @@ -100,7 +100,6 @@
     9.4          Report, Computer Lab, University of Cambridge (1995).
     9.5          http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
     9.6    *}
     9.7 -  options [document = false]
     9.8    theories ECR
     9.9  
    9.10  session "ZF-Constructible" in Constructible = ZF +
    9.11 @@ -198,7 +197,6 @@
    9.12      Porting Experiment.
    9.13      http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
    9.14    *}
    9.15 -  options [document = false]
    9.16    theories Confluence
    9.17  
    9.18  session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
    9.19 @@ -208,7 +206,6 @@
    9.20  
    9.21      ZF/UNITY proofs.
    9.22    *}
    9.23 -  options [document = false]
    9.24    theories
    9.25      (*Simple examples: no composition*)
    9.26      Mutex
    9.27 @@ -235,7 +232,6 @@
    9.28      href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
    9.29      describes the package that automates their declaration.
    9.30    *}
    9.31 -  options [document = false]
    9.32    theories
    9.33      misc
    9.34      Ring             (*abstract algebra*)