src/FOLP/ROOT
changeset 69272 15e9ed5b28fb
parent 66946 3d8fd98c7c86
child 69319 baccaf89ca0d
--- a/src/FOLP/ROOT	Thu Nov 08 22:02:07 2018 +0100
+++ b/src/FOLP/ROOT	Thu Nov 08 22:29:09 2018 +0100
@@ -1,25 +1,25 @@
 chapter FOLP
 
 session FOLP = Pure +
-  description {*
+  description \<open>
     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 {*
+  description \<open>
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
     Examples for First-Order Logic.
-  *}
+\<close>
   theories
     Intro
     Nat