--- 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
--- 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
--- 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
--- 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
--- 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
-
--- 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
--- 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
--- 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*)