diff -r 4cb70e7e36b9 -r 15e9ed5b28fb src/ZF/ROOT
--- a/src/ZF/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/ZF/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,7 +1,7 @@
 chapter ZF
 
 session ZF (main timing) = Pure +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -41,7 +41,7 @@
 
     Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
     (North-Holland, 1980)
-  *}
+\<close>
   sessions
     FOL
   theories
@@ -50,7 +50,7 @@
   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
 
@@ -63,7 +63,7 @@
     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
@@ -78,7 +78,7 @@
   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
 
@@ -99,11 +99,11 @@
         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.
 
@@ -121,7 +121,7 @@
 
     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
@@ -129,7 +129,7 @@
   document_files "root.tex" "root.bib"
 
 session "ZF-IMP" in IMP = ZF +
-  description {*
+  description \<open>
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
@@ -141,19 +141,19 @@
 
     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*)
@@ -181,7 +181,7 @@
     "root.tex"
 
 session "ZF-Resid" in Resid = ZF +
-  description {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -196,16 +196,16 @@
     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
@@ -217,7 +217,7 @@
     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
 
@@ -231,7 +231,7 @@
     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*)