# HG changeset patch # User wenzelm # Date 1509390250 -3600 # Node ID 3d8fd98c7c8614117c531cc5f5624627f21c7931 # Parent b6f787a17fbe18b0f4b3d12d0f0c2402b1087940 ROOT cleanup: empty 'document_files' means there is no document; diff -r b6f787a17fbe -r 3d8fd98c7c86 src/Benchmarks/ROOT --- 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 diff -r b6f787a17fbe -r 3d8fd98c7c86 src/CCL/ROOT --- 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" - diff -r b6f787a17fbe -r 3d8fd98c7c86 src/Cube/ROOT --- 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 - diff -r b6f787a17fbe -r 3d8fd98c7c86 src/Doc/ROOT --- 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 diff -r b6f787a17fbe -r 3d8fd98c7c86 src/FOLP/ROOT --- 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 - diff -r b6f787a17fbe -r 3d8fd98c7c86 src/HOL/ROOT --- 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 diff -r b6f787a17fbe -r 3d8fd98c7c86 src/LCF/ROOT --- 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" - diff -r b6f787a17fbe -r 3d8fd98c7c86 src/Sequents/ROOT --- 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" - diff -r b6f787a17fbe -r 3d8fd98c7c86 src/ZF/ROOT --- 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*)