--- a/src/LCF/ROOT Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ROOT Tue Nov 11 13:40:13 2014 +0100
@@ -11,19 +11,12 @@
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
*}
options [document = false]
- theories LCF
-
-session "LCF-ex" in ex = LCF +
- description {*
- Author: Tobias Nipkow
- Copyright 1991 University of Cambridge
+ theories
+ LCF
- Some examples from Lawrence Paulson's book Logic and Computation.
- *}
- options [document = false]
- theories
- Ex1
- Ex2
- Ex3
- Ex4
+ (* Some examples from Lawrence Paulson's book Logic and Computation *)
+ "ex/Ex1"
+ "ex/Ex2"
+ "ex/Ex3"
+ "ex/Ex4"