--- a/src/LCF/ROOT Tue Nov 20 13:44:06 2018 +0100
+++ b/src/LCF/ROOT Tue Nov 20 13:46:13 2018 +0100
@@ -1,7 +1,7 @@
chapter LCF
session LCF = Pure +
- description \<open>
+ description "
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
@@ -9,12 +9,11 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-\<close>
+ "
sessions
FOL
theories
LCF
-
(* Some examples from Lawrence Paulson's book Logic and Computation *)
"ex/Ex1"
"ex/Ex2"