merged
authorwenzelm
Mon Oct 30 20:27:25 2017 +0100 (19 months ago)
changeset 66951dd4710b91277
parent 66941 c67bb79a0ceb
parent 66950 1a5e90026391
child 66952 80985b62029d
merged
     1.1 --- a/NEWS	Mon Oct 30 17:20:56 2017 +0000
     1.2 +++ b/NEWS	Mon Oct 30 20:27:25 2017 +0100
     1.3 @@ -69,6 +69,10 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* Session ROOT entry: empty 'document_files' means there is no document
     1.8 +for this session. There is no need to specify options [document = false]
     1.9 +anymore.
    1.10 +
    1.11  * Linux and Windows/Cygwin is for x86_64 only. Old 32bit platform
    1.12  support has been discontinued.
    1.13  
     2.1 --- a/lib/Tools/mkroot	Mon Oct 30 17:20:56 2017 +0000
     2.2 +++ b/lib/Tools/mkroot	Mon Oct 30 20:27:25 2017 +0100
     2.3 @@ -101,7 +101,6 @@
     2.4  else
     2.5    cat > "$DIR/ROOT" <<EOF
     2.6  session "$NAME" = "$ISABELLE_LOGIC" +
     2.7 -  options [document = false]
     2.8    theories
     2.9      (* Foo *)
    2.10      (* Bar *)
     3.1 --- a/src/Benchmarks/ROOT	Mon Oct 30 17:20:56 2017 +0000
     3.2 +++ b/src/Benchmarks/ROOT	Mon Oct 30 20:27:25 2017 +0100
     3.3 @@ -4,7 +4,6 @@
     3.4    description {*
     3.5      Big (co)datatypes.
     3.6    *}
     3.7 -  options [document = false]
     3.8    theories
     3.9      Brackin
    3.10      IsaFoR
    3.11 @@ -21,6 +20,5 @@
    3.12    description {*
    3.13      Big records.
    3.14    *}
    3.15 -  options [document = false]
    3.16    theories
    3.17      Record_Benchmark
     4.1 --- a/src/CCL/ROOT	Mon Oct 30 17:20:56 2017 +0000
     4.2 +++ b/src/CCL/ROOT	Mon Oct 30 20:27:25 2017 +0100
     4.3 @@ -10,7 +10,6 @@
     4.4      A computational logic for an untyped functional language with
     4.5      evaluation to weak head-normal form.
     4.6    *}
     4.7 -  options [document = false]
     4.8    sessions
     4.9      FOL
    4.10    theories
    4.11 @@ -22,4 +21,3 @@
    4.12      "ex/List"
    4.13      "ex/Stream"
    4.14      "ex/Flag"
    4.15 -
     5.1 --- a/src/Cube/ROOT	Mon Oct 30 17:20:56 2017 +0000
     5.2 +++ b/src/Cube/ROOT	Mon Oct 30 20:27:25 2017 +0100
     5.3 @@ -13,6 +13,4 @@
     5.4      For more information about the Lambda-Cube, see H. Barendregt, Introduction
     5.5      to Generalised Type Systems, J. Functional Programming.
     5.6    *}
     5.7 -  options [document = false]
     5.8    theories Example
     5.9 -
     6.1 --- a/src/Doc/ROOT	Mon Oct 30 17:20:56 2017 +0000
     6.2 +++ b/src/Doc/ROOT	Mon Oct 30 20:27:25 2017 +0100
     6.3 @@ -17,7 +17,6 @@
     6.4      "style.sty"
     6.5  
     6.6  session Codegen_Basics in "Codegen" = "HOL-Library" +
     6.7 -  options [document = false]
     6.8    theories
     6.9      Setup
    6.10  
    6.11 @@ -505,6 +504,5 @@
    6.12      "style.sty"
    6.13  
    6.14  session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
    6.15 -  options [document = false]
    6.16    theories
    6.17      Setup
     7.1 --- a/src/Doc/System/Environment.thy	Mon Oct 30 17:20:56 2017 +0000
     7.2 +++ b/src/Doc/System/Environment.thy	Mon Oct 30 20:27:25 2017 +0100
     7.3 @@ -255,8 +255,8 @@
     7.4    "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
     7.5    to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
     7.6    \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
     7.7 -  directory). For example: @{verbatim [display] \<open>init_component
     7.8 -  "$HOME/screwdriver-2.0"\<close>}
     7.9 +  directory). For example:
    7.10 +  @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
    7.11  
    7.12    This is tolerant wrt.\ missing component directories, but might produce a
    7.13    warning.
     8.1 --- a/src/FOLP/ROOT	Mon Oct 30 17:20:56 2017 +0000
     8.2 +++ b/src/FOLP/ROOT	Mon Oct 30 20:27:25 2017 +0100
     8.3 @@ -9,7 +9,6 @@
     8.4  
     8.5      Presence of unknown proof term means that matching does not behave as expected.
     8.6    *}
     8.7 -  options [document = false]
     8.8    theories
     8.9      IFOLP (global)
    8.10      FOLP (global)
    8.11 @@ -21,7 +20,6 @@
    8.12  
    8.13      Examples for First-Order Logic.
    8.14    *}
    8.15 -  options [document = false]
    8.16    theories
    8.17      Intro
    8.18      Nat
    8.19 @@ -33,4 +31,3 @@
    8.20      Quantifiers_Int
    8.21      Propositional_Cla
    8.22      Quantifiers_Cla
    8.23 -
     9.1 --- a/src/HOL/ROOT	Mon Oct 30 17:20:56 2017 +0000
     9.2 +++ b/src/HOL/ROOT	Mon Oct 30 20:27:25 2017 +0100
     9.3 @@ -15,7 +15,7 @@
     9.4    description {*
     9.5      HOL-Main with explicit proof terms.
     9.6    *}
     9.7 -  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     9.8 +  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
     9.9    sessions
    9.10      "HOL-Library"
    9.11    theories
    9.12 @@ -177,7 +177,6 @@
    9.13      procedures. For documentation see "Hoare Logic for Mutual Recursion and
    9.14      Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
    9.15    *}
    9.16 -  options [document = false]
    9.17    theories EvenOdd
    9.18  
    9.19  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
    9.20 @@ -233,7 +232,7 @@
    9.21    document_files "root.bib" "root.tex"
    9.22  
    9.23  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
    9.24 -  options [document = false, browser_info = false]
    9.25 +  options [browser_info = false]
    9.26    sessions
    9.27      "HOL-Data_Structures"
    9.28      "HOL-ex"
    9.29 @@ -261,7 +260,6 @@
    9.30  
    9.31      Testing Metis and Sledgehammer.
    9.32    *}
    9.33 -  options [document = false]
    9.34    sessions
    9.35      "HOL-Decision_Procs"
    9.36    theories
    9.37 @@ -280,7 +278,6 @@
    9.38      Author:     Jasmin Blanchette, TU Muenchen
    9.39      Copyright   2009
    9.40    *}
    9.41 -  options [document = false]
    9.42    theories [quick_and_dirty] Nitpick_Examples
    9.43  
    9.44  session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
    9.45 @@ -384,12 +381,10 @@
    9.46    description {*
    9.47      Various decision procedures, typically involving reflection.
    9.48    *}
    9.49 -  options [document = false]
    9.50    theories
    9.51      Decision_Procs
    9.52  
    9.53  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    9.54 -  options [document = false]
    9.55    sessions
    9.56      "HOL-Isar_Examples"
    9.57    theories
    9.58 @@ -443,7 +438,6 @@
    9.59      including some minimal examples (in Test.thy) and a more typical example of
    9.60      a little functional language and its type system.
    9.61    *}
    9.62 -  options [document = false]
    9.63    theories Test Type
    9.64  
    9.65  session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
    9.66 @@ -505,7 +499,6 @@
    9.67      year=1995}
    9.68      ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
    9.69    *}
    9.70 -  options [document = false]
    9.71    theories Solve
    9.72  
    9.73  session "HOL-Lattice" in Lattice = HOL +
    9.74 @@ -521,7 +514,6 @@
    9.75    description {*
    9.76      Miscellaneous examples for Higher-Order Logic.
    9.77    *}
    9.78 -  options [document = false]
    9.79    theories
    9.80      Adhoc_Overloading_Examples
    9.81      Antiquote
    9.82 @@ -667,19 +659,15 @@
    9.83    description {*
    9.84      Lamport's Temporal Logic of Actions.
    9.85    *}
    9.86 -  options [document = false]
    9.87    theories TLA
    9.88  
    9.89  session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
    9.90 -  options [document = false]
    9.91    theories Inc
    9.92  
    9.93  session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
    9.94 -  options [document = false]
    9.95    theories DBuffer
    9.96  
    9.97  session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
    9.98 -  options [document = false]
    9.99    theories MemoryImplementation
   9.100  
   9.101  session "HOL-TPTP" in TPTP = "HOL-Library" +
   9.102 @@ -690,7 +678,6 @@
   9.103  
   9.104      TPTP-related extensions.
   9.105    *}
   9.106 -  options [document = false]
   9.107    theories
   9.108      ATP_Theory_Export
   9.109      MaSh_Eval
   9.110 @@ -712,12 +699,10 @@
   9.111      Measure_Not_CCC
   9.112  
   9.113  session "HOL-Nominal" in Nominal = "HOL-Library" +
   9.114 -  options [document = false]
   9.115    theories
   9.116      Nominal
   9.117  
   9.118  session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   9.119 -  options [document = false]
   9.120    theories
   9.121      Class3
   9.122      CK_Machine
   9.123 @@ -758,7 +743,6 @@
   9.124    description {*
   9.125      (Co)datatype Examples.
   9.126    *}
   9.127 -  options [document = false]
   9.128    theories
   9.129      Compat
   9.130      Lambda_Term
   9.131 @@ -779,7 +763,6 @@
   9.132    description {*
   9.133      Corecursion Examples.
   9.134    *}
   9.135 -  options [document = false]
   9.136    theories
   9.137      LFilter
   9.138      Paper_Examples
   9.139 @@ -807,7 +790,6 @@
   9.140    document_files "root.bib" "root.tex"
   9.141  
   9.142  session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   9.143 -  options [document = false]
   9.144    theories WordExamples
   9.145  
   9.146  session "HOL-Statespace" in Statespace = HOL +
   9.147 @@ -824,20 +806,18 @@
   9.148    document_files "root.tex"
   9.149  
   9.150  session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   9.151 -  options [document = false]
   9.152    theories
   9.153      NSPrimes
   9.154  
   9.155  session "HOL-Mirabelle" in Mirabelle = HOL +
   9.156 -  options [document = false]
   9.157    theories Mirabelle_Test
   9.158  
   9.159  session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   9.160 -  options [document = false, timeout = 60]
   9.161 +  options [timeout = 60]
   9.162    theories Ex
   9.163  
   9.164  session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   9.165 -  options [document = false, quick_and_dirty]
   9.166 +  options [quick_and_dirty]
   9.167    theories
   9.168      Boogie
   9.169      SMT_Examples
   9.170 @@ -845,12 +825,11 @@
   9.171      SMT_Tests
   9.172  
   9.173  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   9.174 -  options [document = false]
   9.175    theories
   9.176      SPARK (global)
   9.177  
   9.178  session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   9.179 -  options [document = false, spark_prv = false]
   9.180 +  options [spark_prv = false]
   9.181    theories
   9.182      "Gcd/Greatest_Common_Divisor"
   9.183      "Liseq/Longest_Increasing_Subsequence"
   9.184 @@ -889,11 +868,9 @@
   9.185      "Simple_Gcd.ads"
   9.186  
   9.187  session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   9.188 -  options [document = false]
   9.189    theories MutabelleExtra
   9.190  
   9.191  session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
   9.192 -  options [document = false]
   9.193    theories
   9.194      Quickcheck_Examples
   9.195      Quickcheck_Lattice_Examples
   9.196 @@ -908,7 +885,6 @@
   9.197    description {*
   9.198      Author:     Cezary Kaliszyk and Christian Urban
   9.199    *}
   9.200 -  options [document = false]
   9.201    theories
   9.202      DList
   9.203      Quotient_FSet
   9.204 @@ -923,7 +899,6 @@
   9.205      Lifting_Code_Dt_Test
   9.206  
   9.207  session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
   9.208 -  options [document = false]
   9.209    theories
   9.210      Examples
   9.211      Predicate_Compile_Tests
   9.212 @@ -948,7 +923,6 @@
   9.213    description {*
   9.214      Experimental extension of Higher-Order Logic to allow translation of types to sets.
   9.215    *}
   9.216 -  options [document = false]
   9.217    theories
   9.218      Types_To_Sets
   9.219      "Examples/Prerequisites"
   9.220 @@ -974,7 +948,6 @@
   9.221    document_files "root.tex"
   9.222  
   9.223  session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   9.224 -  options [document = false]
   9.225    theories
   9.226      HOLCF_Library
   9.227      HOL_Cpo
   9.228 @@ -985,18 +958,19 @@
   9.229  
   9.230      This is the HOLCF-based denotational semantics of a simple WHILE-language.
   9.231    *}
   9.232 -  options [document = false]
   9.233    sessions
   9.234      "HOL-IMP"
   9.235    theories
   9.236      HoareEx
   9.237 -  document_files "root.tex"
   9.238 +  document_files
   9.239 +    "isaverbatimwrite.sty"
   9.240 +    "root.tex"
   9.241 +    "root.bib"
   9.242  
   9.243  session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   9.244    description {*
   9.245      Miscellaneous examples for HOLCF.
   9.246    *}
   9.247 -  options [document = false]
   9.248    theories
   9.249      Dnat
   9.250      Dagstuhl
   9.251 @@ -1025,7 +999,6 @@
   9.252      "Specification and Development of Interactive Systems: Focus on Streams,
   9.253      Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
   9.254    *}
   9.255 -  options [document = false]
   9.256    theories
   9.257      Fstreams
   9.258      FOCUS
   9.259 @@ -1042,7 +1015,6 @@
   9.260      abstraction theory. Everything is based upon a domain-theoretic model of
   9.261      finite and infinite sequences.
   9.262    *}
   9.263 -  options [document = false]
   9.264    theories Abstraction
   9.265  
   9.266  session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   9.267 @@ -1051,7 +1023,6 @@
   9.268  
   9.269      The Alternating Bit Protocol performed in I/O-Automata.
   9.270    *}
   9.271 -  options [document = false]
   9.272    theories
   9.273      Correctness
   9.274      Spec
   9.275 @@ -1063,7 +1034,6 @@
   9.276      A network transmission protocol, performed in the
   9.277      I/O automata formalization by Olaf Mueller.
   9.278    *}
   9.279 -  options [document = false]
   9.280    theories Correctness
   9.281  
   9.282  session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   9.283 @@ -1072,14 +1042,12 @@
   9.284  
   9.285      Memory storage case study.
   9.286    *}
   9.287 -  options [document = false]
   9.288    theories Correctness
   9.289  
   9.290  session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   9.291    description {*
   9.292      Author:     Olaf Mueller
   9.293    *}
   9.294 -  options [document = false]
   9.295    theories
   9.296      TrivEx
   9.297      TrivEx2
    10.1 --- a/src/LCF/ROOT	Mon Oct 30 17:20:56 2017 +0000
    10.2 +++ b/src/LCF/ROOT	Mon Oct 30 20:27:25 2017 +0100
    10.3 @@ -10,7 +10,6 @@
    10.4      Useful references on LCF: Lawrence C. Paulson,
    10.5      Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
    10.6    *}
    10.7 -  options [document = false]
    10.8    sessions
    10.9      FOL
   10.10    theories
   10.11 @@ -21,4 +20,3 @@
   10.12      "ex/Ex2"
   10.13      "ex/Ex3"
   10.14      "ex/Ex4"
   10.15 -
    11.1 --- a/src/Pure/Admin/build_log.scala	Mon Oct 30 17:20:56 2017 +0000
    11.2 +++ b/src/Pure/Admin/build_log.scala	Mon Oct 30 20:27:25 2017 +0100
    11.3 @@ -649,6 +649,10 @@
    11.4      ml_statistics: List[Properties.T],
    11.5      task_statistics: List[Properties.T],
    11.6      errors: List[String])
    11.7 +  {
    11.8 +    def error(s: String): Session_Info =
    11.9 +      copy(errors = errors ::: List(s))
   11.10 +  }
   11.11  
   11.12    private def parse_session_info(
   11.13      log_file: Log_File,
    12.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 30 17:20:56 2017 +0000
    12.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 30 20:27:25 2017 +0100
    12.3 @@ -392,13 +392,6 @@
    12.4    }
    12.5  
    12.6  
    12.7 -  /* protocol functions */
    12.8 -
    12.9 -  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
   12.10 -
   12.11 -  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
   12.12 -
   12.13 -
   12.14    /* command indentation */
   12.15  
   12.16    object Command_Indent
   12.17 @@ -506,6 +499,9 @@
   12.18    val FUNCTION = "function"
   12.19    val Function = new Properties.String(FUNCTION)
   12.20  
   12.21 +  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
   12.22 +  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
   12.23 +
   12.24    val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   12.25    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
   12.26  
    13.1 --- a/src/Pure/Thy/present.ML	Mon Oct 30 17:20:56 2017 +0000
    13.2 +++ b/src/Pure/Thy/present.ML	Mon Oct 30 20:27:25 2017 +0100
    13.3 @@ -171,13 +171,7 @@
    13.4        val doc_output =
    13.5          if document_output = "" then NONE else SOME (Path.explode document_output);
    13.6  
    13.7 -      val documents =
    13.8 -        if doc = "" then []
    13.9 -        else if null doc_files andalso not (can File.check_dir document_path) then
   13.10 -          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
   13.11 -           else (); [])
   13.12 -        else doc_variants;
   13.13 -
   13.14 +      val documents = if doc = "" orelse null doc_files then [] else doc_variants;
   13.15        val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
   13.16  
   13.17        val docs =
    14.1 --- a/src/Pure/Tools/build.scala	Mon Oct 30 17:20:56 2017 +0000
    14.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 30 20:27:25 2017 +0100
    14.3 @@ -298,11 +298,10 @@
    14.4      def terminate: Unit = future_result.cancel
    14.5      def is_finished: Boolean = future_result.is_finished
    14.6  
    14.7 -    @volatile private var was_timeout = false
    14.8      private val timeout_request: Option[Event_Timer.Request] =
    14.9      {
   14.10        if (info.timeout > Time.zero)
   14.11 -        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
   14.12 +        Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
   14.13        else None
   14.14      }
   14.15  
   14.16 @@ -314,7 +313,12 @@
   14.17          Present.finish(progress, store.browser_info, graph_file, info, name)
   14.18  
   14.19        graph_file.delete
   14.20 -      timeout_request.foreach(_.cancel)
   14.21 +
   14.22 +      val was_timeout =
   14.23 +        timeout_request match {
   14.24 +          case None => false
   14.25 +          case Some(request) => !request.cancel
   14.26 +        }
   14.27  
   14.28        if (result.interrupted) {
   14.29          if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   14.30 @@ -532,15 +536,18 @@
   14.31                val database = store.output_dir + store.database(name)
   14.32                database.file.delete
   14.33  
   14.34 +              val build_log =
   14.35 +                Build_Log.Log_File(name, process_result.out_lines).
   14.36 +                  parse_session_info(
   14.37 +                    command_timings = true,
   14.38 +                    theory_timings = true,
   14.39 +                    ml_statistics = true,
   14.40 +                    task_statistics = true)
   14.41 +
   14.42                using(SQLite.open_database(database))(db =>
   14.43                  store.write_session_info(db, name,
   14.44                    build_log =
   14.45 -                    Build_Log.Log_File(name, process_result.out_lines).
   14.46 -                      parse_session_info(
   14.47 -                        command_timings = true,
   14.48 -                        theory_timings = true,
   14.49 -                        ml_statistics = true,
   14.50 -                        task_statistics = true),
   14.51 +                    if (process_result.timeout) build_log.error("Timeout") else build_log,
   14.52                    build =
   14.53                      Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   14.54                        process_result.rc)))
    15.1 --- a/src/Sequents/ROOT	Mon Oct 30 17:20:56 2017 +0000
    15.2 +++ b/src/Sequents/ROOT	Mon Oct 30 20:27:25 2017 +0100
    15.3 @@ -37,7 +37,6 @@
    15.4      S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
    15.5      of Cambridge Computer Lab, 1995, ed L. Paulson)
    15.6    *}
    15.7 -  options [document = false]
    15.8    theories
    15.9      LK
   15.10      ILL
   15.11 @@ -53,4 +52,3 @@
   15.12      "LK/Quantifiers"
   15.13      "LK/Hard_Quantifiers"
   15.14      "LK/Nat"
   15.15 -
    16.1 --- a/src/ZF/ROOT	Mon Oct 30 17:20:56 2017 +0000
    16.2 +++ b/src/ZF/ROOT	Mon Oct 30 20:27:25 2017 +0100
    16.3 @@ -100,7 +100,6 @@
    16.4          Report, Computer Lab, University of Cambridge (1995).
    16.5          http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
    16.6    *}
    16.7 -  options [document = false]
    16.8    theories ECR
    16.9  
   16.10  session "ZF-Constructible" in Constructible = ZF +
   16.11 @@ -198,7 +197,6 @@
   16.12      Porting Experiment.
   16.13      http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   16.14    *}
   16.15 -  options [document = false]
   16.16    theories Confluence
   16.17  
   16.18  session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
   16.19 @@ -208,7 +206,6 @@
   16.20  
   16.21      ZF/UNITY proofs.
   16.22    *}
   16.23 -  options [document = false]
   16.24    theories
   16.25      (*Simple examples: no composition*)
   16.26      Mutex
   16.27 @@ -235,7 +232,6 @@
   16.28      href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
   16.29      describes the package that automates their declaration.
   16.30    *}
   16.31 -  options [document = false]
   16.32    theories
   16.33      misc
   16.34      Ring             (*abstract algebra*)