# HG changeset patch
# User wenzelm
# Date 1343155354 -7200
# Node ID 9bfb6978eb80dbdb578e24872d1f79cce1123e2b
# Parent  45137257399ad116838165a42ba64e8ae5196c48
more explicit document = false to reduce warnings;
tuned;

diff -r 45137257399a -r 9bfb6978eb80 src/CCL/ROOT
--- a/src/CCL/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/CCL/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -8,6 +8,7 @@
     A computational logic for an untyped functional language with
     evaluation to weak head-normal form.
   *}
+  options [document = false]
   theories Wfd Fix
 
 session ex = CCL +
@@ -17,5 +18,6 @@
 
     Examples for Classical Computational Logic.
   *}
+  options [document = false]
   theories Nat List Stream Flag
 
diff -r 45137257399a -r 9bfb6978eb80 src/CTT/ROOT
--- a/src/CTT/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/CTT/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -3,6 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
   *}
+  options [document = false]
   theories Main
 
 session ex = CTT +
@@ -12,4 +13,5 @@
 
     Examples for Constructive Type Theory.
   *}
+  options [document = false]
   theories Typechecking Elimination Equality Synthesis
diff -r 45137257399a -r 9bfb6978eb80 src/Cube/ROOT
--- a/src/Cube/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/Cube/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -5,5 +5,6 @@
 
     The Lambda-Cube a la Barendregt.
   *}
+  options [document = false]
   theories Example
 
diff -r 45137257399a -r 9bfb6978eb80 src/FOLP/ROOT
--- a/src/FOLP/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/FOLP/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -7,6 +7,7 @@
 
     Presence of unknown proof term means that matching does not behave as expected.
   *}
+  options [document = false]
   theories FOLP
 
 session ex = FOLP +
@@ -16,6 +17,7 @@
 
     Examples for First-Order Logic.
   *}
+  options [document = false]
   theories
     Intro
     Nat
diff -r 45137257399a -r 9bfb6978eb80 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -114,6 +114,7 @@
     Author:     David von Oheimb
     Copyright   1999 TUM
   *}
+  options [document = false]
   theories EvenOdd
 
 session Import = HOL +
@@ -122,6 +123,7 @@
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session Number_Theory = HOL +
+  options [document = false]
   theories Number_Theory
 
 session Old_Number_Theory = HOL +
@@ -160,6 +162,7 @@
 
     Testing Metis and Sledgehammer.
   *}
+  options [document = false]
   theories
     Abstraction
     Big_O
@@ -176,6 +179,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
   *}
+  options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
 session Algebra = HOL +
@@ -286,10 +290,11 @@
   files "document/root.bib" "document/root.tex"
 
 session Decision_Procs = HOL +
+  options [document = false]
   theories Decision_Procs
 
 session ex in "Proofs/ex" = "HOL-Proofs" +
-  options [proofs = 2, parallel_proofs = 0]
+  options [document = false, proofs = 2, parallel_proofs = 0]
   theories Hilbert_Classical
 
 session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
@@ -324,6 +329,7 @@
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   *}
+  options [document = false]
   theories Test Type
 
 session MicroJava = HOL +
@@ -375,6 +381,7 @@
     year=1995}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   *}
+  options [document = false]
   theories Solve
 
 session Lattice = HOL +
@@ -509,15 +516,19 @@
 
 session TLA! = HOL +
   description {* The Temporal Logic of Actions *}
+  options [document = false]
   theories TLA
 
 session Inc in "TLA/Inc" = TLA +
+  options [document = false]
   theories Inc
 
 session Buffer in "TLA/Buffer" = TLA +
+  options [document = false]
   theories DBuffer
 
 session Memory in "TLA/Memory" = TLA +
+  options [document = false]
   theories MemoryImplementation
 
 session TPTP = HOL +
@@ -528,6 +539,7 @@
 
     TPTP-related extensions.
   *}
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -559,9 +571,11 @@
   files "document/root.tex"
 
 session Nominal = HOL +
+  options [document = false]
   theories Nominal
 
 session Examples in "Nominal/Examples" = "HOL-Nominal" +
+  options [document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
@@ -571,6 +585,7 @@
   files "document/root.bib" "document/root.tex"
 
 session Examples in "Word/Examples" = "HOL-Word" +
+  options [document = false]
   theories WordExamples
 
 session Statespace = HOL +
@@ -583,16 +598,18 @@
   files "document/root.tex"
 
 session Examples in "NSA/Examples" = "HOL-NSA" +
+  options [document = false]
   theories NSPrimes
 
 session Mirabelle = HOL +
+  options [document = false]
   theories Mirabelle_Test
 (* FIXME
 	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
 *)
 
 session SMT_Examples = "HOL-Word" +
-  options [quick_and_dirty]
+  options [document = false, quick_and_dirty]
   theories
     SMT_Tests
     SMT_Examples
@@ -602,10 +619,12 @@
     "SMT_Tests.certs"
 
 session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+  options [document = false]
   theories Boogie
   (* FIXME files!?! *)
 
 session Examples in "Boogie/Examples" = "HOL-Boogie" +
+  options [document = false]
   theories
     Boogie_Max_Stepwise
     Boogie_Max
@@ -617,9 +636,11 @@
     "VCC_Max.certs"
 
 session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+  options [document = false]
   theories SPARK
 
 session Examples in "SPARK/Examples" = "HOL-SPARK" +
+  options [document = false]
   theories
     "Gcd/Greatest_Common_Divisor"
 
@@ -705,15 +726,18 @@
     "simple_greatest_common_divisor/g_c_d.siv"
 
 session Mutabelle = HOL +
+  options [document = false]
   theories MutabelleExtra
 
 session Quickcheck_Examples = HOL +
+  options [document = false]
   theories Quickcheck_Examples  (* FIXME *)
 
 session Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
+  options [document = false]
   theories
     DList
     FSet
@@ -727,6 +751,7 @@
     Lift_DList
 
 session Predicate_Compile_Examples = HOL +
+  options [document = false]
   theories  (* FIXME *)
     Examples
     Predicate_Compile_Tests
@@ -757,14 +782,17 @@
   files "document/root.tex"
 
 session Library in "HOLCF/Library" = HOLCF +
+  options [document = false]
   theories HOLCF_Library
 
 session IMP in "HOLCF/IMP" = HOLCF +
+  options [document = false]
   theories HoareEx
   files "document/root.tex"
 
 session ex in "HOLCF/ex" = HOLCF +
   description {* Misc HOLCF examples *}
+  options [document = false]
   theories
     Dnat
     Dagstuhl
@@ -779,6 +807,7 @@
     Pattern_Match
 
 session FOCUS in "HOLCF/FOCUS" = HOLCF +
+  options [document = false]
   theories
     Fstreams
     FOCUS
@@ -790,6 +819,7 @@
 
     Formalization of a semantic model of I/O-Automata.
   *}
+  options [document = false]
   theories "meta_theory/Abstraction"
 
 session ABP in "HOLCF/IOA/ABP" = IOA +
@@ -798,6 +828,7 @@
 
     The Alternating Bit Protocol performed in I/O-Automata.
   *}
+  options [document = false]
   theories Correctness
 
 session NTP in "HOLCF/IOA/NTP" = IOA +
@@ -807,6 +838,7 @@
     A network transmission protocol, performed in the
     I/O automata formalization by Olaf Mueller.
   *}
+  options [document = false]
   theories Correctness
 
 session Storage in "HOLCF/IOA/Storage" = IOA +
@@ -815,18 +847,21 @@
 
     Memory storage case study.
   *}
+  options [document = false]
   theories Correctness
 
 session ex in "HOLCF/IOA/ex" = IOA +
   description {*
     Author:     Olaf Mueller
   *}
+  options [document = false]
   theories
     TrivEx
     TrivEx2
 
 session Datatype_Benchmark = HOL +
   description {* Some rather large datatype examples (from John Harrison). *}
+  options [document = false]
   theories [condition = ISABELLE_BENCHMARK]
     (* FIXME Toplevel.timing := true; *)
     Brackin
@@ -836,8 +871,8 @@
 
 session Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
+  options [document = false]
   theories [condition = ISABELLE_BENCHMARK]
     (* FIXME Toplevel.timing := true; *)
     Record_Benchmark
 
-
diff -r 45137257399a -r 9bfb6978eb80 src/LCF/ROOT
--- a/src/LCF/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/LCF/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -3,6 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
   *}
+  options [document = false]
   theories LCF
 
 session ex = LCF +
@@ -12,5 +13,10 @@
 
     Some examples from Lawrence Paulson's book Logic and Computation.
   *}
-  theories Ex1 Ex2 Ex3 Ex4
+  options [document = false]
+  theories
+    Ex1
+    Ex2
+    Ex3
+    Ex4
 
diff -r 45137257399a -r 9bfb6978eb80 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/Sequents/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -5,7 +5,16 @@
 
     Classical Sequent Calculus based on Pure Isabelle.
   *}
-  theories LK ILL ILL_predlog Washing Modal0 T S4 S43
+  options [document = false]
+  theories
+    LK
+    ILL
+    ILL_predlog
+    Washing
+    Modal0
+    T
+    S4
+    S43
 
 session LK = Sequents +
   description {*
@@ -14,5 +23,10 @@
 
     Examples for Classical Logic.
   *}
-  theories Propositional Quantifiers Hard_Quantifiers Nat
+  options [document = false]
+  theories
+    Propositional
+    Quantifiers
+    Hard_Quantifiers
+    Nat
 
diff -r 45137257399a -r 9bfb6978eb80 src/ZF/ROOT
--- a/src/ZF/ROOT	Tue Jul 24 20:41:50 2012 +0200
+++ b/src/ZF/ROOT	Tue Jul 24 20:42:34 2012 +0200
@@ -8,7 +8,9 @@
     This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
   *}
   options [document_graph]
-  theories Main Main_ZFC
+  theories
+    Main
+    Main_ZFC
   files "document/root.tex"
 
 session AC = ZF +
@@ -19,8 +21,17 @@
     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
   *}
   options [document_graph]
-  theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6
-    WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC
+  theories
+    WO6_WO1
+    WO1_WO7
+    AC7_AC9
+    WO1_AC
+    AC15_WO6
+    WO2_AC16
+    AC16_WO4
+    AC17_AC1
+    AC18_AC19
+    DC
   files "document/root.tex" "document/root.bib"
 
 session Coind = ZF +
@@ -39,6 +50,7 @@
         Jacob Frost, A Case Study of Co_induction in Isabelle
         Report, Computer Lab, University of Cambridge (1995).
   *}
+  options [document = false]
   theories ECR
 
 session Constructible = ZF +
@@ -61,6 +73,7 @@
     Glynn Winskel. The Formal Semantics of Programming Languages.
     MIT Press, 1993.
   *}
+  options [document = false]
   theories Equiv
   files "document/root.tex" "document/root.bib"
 
@@ -108,6 +121,7 @@
     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
     J. Functional Programming 4(3) 1994, 371-394.
   *}
+  options [document = false]
   theories Confluence
 
 session UNITY = ZF +
@@ -117,6 +131,7 @@
 
     ZF/UNITY proofs.
   *}
+  options [document = false]
   theories
     (*Simple examples: no composition*)
     Mutex
@@ -134,6 +149,7 @@
 
     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   *}
+  options [document = false]
   theories
     misc
     Ring             (*abstract algebra*)