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