src/FOLP/ROOT
changeset 69319 baccaf89ca0d
parent 69272 15e9ed5b28fb
child 75992 1f6d79b62222
--- 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