src/ZF/ROOT

 chapter ZF
 
 session ZF (main timing) = Pure +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
     Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
     Philippe Noel and Lawrence Paulson.

 
     Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
 
     Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
     (North-Holland, 1980)
-  *}
+\<close>
   sessions
     FOL
   theories
     ZF (global)
     ZFC (global)
   document_files "root.tex"
 
 session "ZF-AC" in AC = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
 

 
     The report
     http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
     "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
     development and ZF's theories of cardinals.
-  *}
+\<close>
   theories
     WO6_WO1
     WO1_WO7
     AC7_AC9
     WO1_AC

     AC18_AC19
     DC
   document_files "root.tex" "root.bib"
 
 session "ZF-Coind" in Coind = ZF +
-  description {*
+  description \<open>
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
     Coind -- A Coinduction Example.
 

 
     Written up as
         Jacob Frost, A Case Study of Co_induction in Isabelle
         Report, Computer Lab, University of Cambridge (1995).
         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
-  *}
+\<close>
   theories ECR
 
 session "ZF-Constructible" in Constructible = ZF +
-  description {*
+  description \<open>
     Relative Consistency of the Axiom of Choice:
     Inner Models, Absoluteness and Consistency Proofs.
 
     Gödel's proof of the relative consistency of the axiom of choice is
     mechanized using Isabelle/ZF. The proof builds upon a previous

     of further material from that book. It also serves as an example of what to
     expect when deep mathematics is formalized.
 
     A paper describing this development is
     http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
-  *}
+\<close>
   theories
     DPow_absolute
     AC_in_L
     Rank_Separation
   document_files "root.tex" "root.bib"
 
 session "ZF-IMP" in IMP = ZF +
-  description {*
+  description \<open>
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
     Formalization of the denotational and operational semantics of a
     simple while-language, including an equivalence proof.

     The whole development essentially formalizes/transcribes
     chapters 2 and 5 of
 
     Glynn Winskel. The Formal Semantics of Programming Languages.
     MIT Press, 1993.
-  *}
+\<close>
   theories Equiv
   document_files
     "root.tex"
     "root.bib"
 
 session "ZF-Induct" in Induct = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
     Inductive definitions.
-  *}
+\<close>
   theories
     (** Datatypes **)
     Datatypes       (*sample datatypes*)
     Binary_Trees    (*binary trees*)
     Term            (*recursion over the list functor*)

   document_files
     "root.bib"
     "root.tex"
 
 session "ZF-Resid" in Resid = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
     Residuals -- a proof of the Church-Rosser Theorem for the
     untyped lambda-calculus.

     J. Functional Programming 4(3) 1994, 371-394.
 
     See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
     Porting Experiment.
     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
-  *}
+\<close>
   theories Confluence
 
 session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     ZF/UNITY proofs.
-  *}
+\<close>
   theories
     (*Simple examples: no composition*)
     Mutex
 
     (*Basic meta-theory*)

 
     (*Prefix relation; the Allocator example*)
     Distributor Merge ClientImpl AllocImpl
 
 session "ZF-ex" in ex = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
 

     Several (co)inductive and (co)datatype definitions are presented. The
     report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
     describes the theoretical foundations of datatypes while
     href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
     describes the package that automates their declaration.
-  *}
+\<close>
   theories
     misc
     Ring             (*abstract algebra*)
     Commutation      (*abstract Church-Rosser theory*)
     Primes           (*GCD theory*)