--- a/src/Benchmarks/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/Benchmarks/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -4,7 +4,6 @@
description {*
Big (co)datatypes.
*}
- options [document = false]
theories
Brackin
IsaFoR
@@ -21,6 +20,5 @@
description {*
Big records.
*}
- options [document = false]
theories
Record_Benchmark
--- a/src/CCL/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/CCL/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -10,7 +10,6 @@
A computational logic for an untyped functional language with
evaluation to weak head-normal form.
*}
- options [document = false]
sessions
FOL
theories
@@ -22,4 +21,3 @@
"ex/List"
"ex/Stream"
"ex/Flag"
-
--- a/src/Cube/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/Cube/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -13,6 +13,4 @@
For more information about the Lambda-Cube, see H. Barendregt, Introduction
to Generalised Type Systems, J. Functional Programming.
*}
- options [document = false]
theories Example
-
--- a/src/Doc/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/Doc/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -17,7 +17,6 @@
"style.sty"
session Codegen_Basics in "Codegen" = "HOL-Library" +
- options [document = false]
theories
Setup
@@ -505,6 +504,5 @@
"style.sty"
session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
- options [document = false]
theories
Setup
--- a/src/FOLP/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/FOLP/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -9,7 +9,6 @@
Presence of unknown proof term means that matching does not behave as expected.
*}
- options [document = false]
theories
IFOLP (global)
FOLP (global)
@@ -21,7 +20,6 @@
Examples for First-Order Logic.
*}
- options [document = false]
theories
Intro
Nat
@@ -33,4 +31,3 @@
Quantifiers_Int
Propositional_Cla
Quantifiers_Cla
-
--- a/src/HOL/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/HOL/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -15,7 +15,7 @@
description {*
HOL-Main with explicit proof terms.
*}
- options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
+ options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
sessions
"HOL-Library"
theories
@@ -177,7 +177,6 @@
procedures. For documentation see "Hoare Logic for Mutual Recursion and
Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
*}
- options [document = false]
theories EvenOdd
session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
@@ -233,7 +232,7 @@
document_files "root.bib" "root.tex"
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
- options [document = false, browser_info = false]
+ options [browser_info = false]
sessions
"HOL-Data_Structures"
"HOL-ex"
@@ -261,7 +260,6 @@
Testing Metis and Sledgehammer.
*}
- options [document = false]
sessions
"HOL-Decision_Procs"
theories
@@ -280,7 +278,6 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
*}
- options [document = false]
theories [quick_and_dirty] Nitpick_Examples
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
@@ -384,12 +381,10 @@
description {*
Various decision procedures, typically involving reflection.
*}
- options [document = false]
theories
Decision_Procs
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
- options [document = false]
sessions
"HOL-Isar_Examples"
theories
@@ -443,7 +438,6 @@
including some minimal examples (in Test.thy) and a more typical example of
a little functional language and its type system.
*}
- options [document = false]
theories Test Type
session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
@@ -505,7 +499,6 @@
year=1995}
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
*}
- options [document = false]
theories Solve
session "HOL-Lattice" in Lattice = HOL +
@@ -521,7 +514,6 @@
description {*
Miscellaneous examples for Higher-Order Logic.
*}
- options [document = false]
theories
Adhoc_Overloading_Examples
Antiquote
@@ -667,19 +659,15 @@
description {*
Lamport's Temporal Logic of Actions.
*}
- options [document = false]
theories TLA
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
- options [document = false]
theories Inc
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
- options [document = false]
theories DBuffer
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
- options [document = false]
theories MemoryImplementation
session "HOL-TPTP" in TPTP = "HOL-Library" +
@@ -690,7 +678,6 @@
TPTP-related extensions.
*}
- options [document = false]
theories
ATP_Theory_Export
MaSh_Eval
@@ -712,12 +699,10 @@
Measure_Not_CCC
session "HOL-Nominal" in Nominal = "HOL-Library" +
- options [document = false]
theories
Nominal
session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
- options [document = false]
theories
Class3
CK_Machine
@@ -758,7 +743,6 @@
description {*
(Co)datatype Examples.
*}
- options [document = false]
theories
Compat
Lambda_Term
@@ -779,7 +763,6 @@
description {*
Corecursion Examples.
*}
- options [document = false]
theories
LFilter
Paper_Examples
@@ -807,7 +790,6 @@
document_files "root.bib" "root.tex"
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
- options [document = false]
theories WordExamples
session "HOL-Statespace" in Statespace = HOL +
@@ -824,20 +806,18 @@
document_files "root.tex"
session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
- options [document = false]
theories
NSPrimes
session "HOL-Mirabelle" in Mirabelle = HOL +
- options [document = false]
theories Mirabelle_Test
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
- options [document = false, timeout = 60]
+ options [timeout = 60]
theories Ex
session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
- options [document = false, quick_and_dirty]
+ options [quick_and_dirty]
theories
Boogie
SMT_Examples
@@ -845,12 +825,11 @@
SMT_Tests
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
- options [document = false]
theories
SPARK (global)
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
- options [document = false, spark_prv = false]
+ options [spark_prv = false]
theories
"Gcd/Greatest_Common_Divisor"
"Liseq/Longest_Increasing_Subsequence"
@@ -889,11 +868,9 @@
"Simple_Gcd.ads"
session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
- options [document = false]
theories MutabelleExtra
session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" +
- options [document = false]
theories
Quickcheck_Examples
Quickcheck_Lattice_Examples
@@ -908,7 +885,6 @@
description {*
Author: Cezary Kaliszyk and Christian Urban
*}
- options [document = false]
theories
DList
Quotient_FSet
@@ -923,7 +899,6 @@
Lifting_Code_Dt_Test
session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" +
- options [document = false]
theories
Examples
Predicate_Compile_Tests
@@ -948,7 +923,6 @@
description {*
Experimental extension of Higher-Order Logic to allow translation of types to sets.
*}
- options [document = false]
theories
Types_To_Sets
"Examples/Prerequisites"
@@ -974,7 +948,6 @@
document_files "root.tex"
session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
- options [document = false]
theories
HOLCF_Library
HOL_Cpo
@@ -985,7 +958,6 @@
This is the HOLCF-based denotational semantics of a simple WHILE-language.
*}
- options [document = false]
sessions
"HOL-IMP"
theories
@@ -996,7 +968,6 @@
description {*
Miscellaneous examples for HOLCF.
*}
- options [document = false]
theories
Dnat
Dagstuhl
@@ -1025,7 +996,6 @@
"Specification and Development of Interactive Systems: Focus on Streams,
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
*}
- options [document = false]
theories
Fstreams
FOCUS
@@ -1042,7 +1012,6 @@
abstraction theory. Everything is based upon a domain-theoretic model of
finite and infinite sequences.
*}
- options [document = false]
theories Abstraction
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
@@ -1051,7 +1020,6 @@
The Alternating Bit Protocol performed in I/O-Automata.
*}
- options [document = false]
theories
Correctness
Spec
@@ -1063,7 +1031,6 @@
A network transmission protocol, performed in the
I/O automata formalization by Olaf Mueller.
*}
- options [document = false]
theories Correctness
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
@@ -1072,14 +1039,12 @@
Memory storage case study.
*}
- options [document = false]
theories Correctness
session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
description {*
Author: Olaf Mueller
*}
- options [document = false]
theories
TrivEx
TrivEx2
--- a/src/LCF/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/LCF/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -10,7 +10,6 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
*}
- options [document = false]
sessions
FOL
theories
@@ -21,4 +20,3 @@
"ex/Ex2"
"ex/Ex3"
"ex/Ex4"
-
--- a/src/Sequents/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/Sequents/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -37,7 +37,6 @@
S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
of Cambridge Computer Lab, 1995, ed L. Paulson)
*}
- options [document = false]
theories
LK
ILL
@@ -53,4 +52,3 @@
"LK/Quantifiers"
"LK/Hard_Quantifiers"
"LK/Nat"
-
--- a/src/ZF/ROOT Mon Oct 30 19:36:27 2017 +0100
+++ b/src/ZF/ROOT Mon Oct 30 20:04:10 2017 +0100
@@ -100,7 +100,6 @@
Report, Computer Lab, University of Cambridge (1995).
http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
*}
- options [document = false]
theories ECR
session "ZF-Constructible" in Constructible = ZF +
@@ -198,7 +197,6 @@
Porting Experiment.
http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
*}
- options [document = false]
theories Confluence
session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
@@ -208,7 +206,6 @@
ZF/UNITY proofs.
*}
- options [document = false]
theories
(*Simple examples: no composition*)
Mutex
@@ -235,7 +232,6 @@
href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
describes the package that automates their declaration.
*}
- options [document = false]
theories
misc
Ring (*abstract algebra*)