src/ZF/ROOT
changeset 66946 3d8fd98c7c86
parent 66778 cf0187ca3a57
child 69272 15e9ed5b28fb
     1.1 --- a/src/ZF/ROOT	Mon Oct 30 19:36:27 2017 +0100
     1.2 +++ b/src/ZF/ROOT	Mon Oct 30 20:04:10 2017 +0100
     1.3 @@ -100,7 +100,6 @@
     1.4          Report, Computer Lab, University of Cambridge (1995).
     1.5          http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
     1.6    *}
     1.7 -  options [document = false]
     1.8    theories ECR
     1.9  
    1.10  session "ZF-Constructible" in Constructible = ZF +
    1.11 @@ -198,7 +197,6 @@
    1.12      Porting Experiment.
    1.13      http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
    1.14    *}
    1.15 -  options [document = false]
    1.16    theories Confluence
    1.17  
    1.18  session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
    1.19 @@ -208,7 +206,6 @@
    1.20  
    1.21      ZF/UNITY proofs.
    1.22    *}
    1.23 -  options [document = false]
    1.24    theories
    1.25      (*Simple examples: no composition*)
    1.26      Mutex
    1.27 @@ -235,7 +232,6 @@
    1.28      href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
    1.29      describes the package that automates their declaration.
    1.30    *}
    1.31 -  options [document = false]
    1.32    theories
    1.33      misc
    1.34      Ring             (*abstract algebra*)