src/ZF/ROOT
changeset 66946 3d8fd98c7c86
parent 66778 cf0187ca3a57
child 69272 15e9ed5b28fb
--- 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*)