diff -r f3351bb4390e -r baccaf89ca0d src/FOLP/ROOT
--- a/src/FOLP/ROOT	Tue Nov 20 13:44:06 2018 +0100
+++ b/src/FOLP/ROOT	Tue Nov 20 13:46:13 2018 +0100
@@ -1,25 +1,25 @@
 chapter FOLP
 
 session FOLP = Pure +
-  description \<open>
+  description "
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
     Modifed version of FOL that contains proof terms.
 
     Presence of unknown proof term means that matching does not behave as expected.
-\<close>
+  "
   theories
     IFOLP (global)
     FOLP (global)
 
 session "FOLP-ex" in ex = FOLP +
-  description \<open>
+  description "
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
     Examples for First-Order Logic.
-\<close>
+  "
   theories
     Intro
     Nat