src/LCF/ex.ML
 changeset 420 1e0f1973536d parent 203 4a213aaca3d9
```--- a/src/LCF/ex.ML	Thu Jun 09 11:09:45 1994 +0200
+++ b/src/LCF/ex.ML	Thu Jun 09 11:11:03 1994 +0200
@@ -1,29 +1,31 @@
-(*  Title: 	LCF/ex.ML
+(*  Title:      LCF/ex.ML
ID:         \$Id\$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow

Some examples from Lawrence Paulson's book Logic and Computation.
*)

-LCF_build_completed;	(*Cause examples to fail if LCF did*)
+LCF_build_completed;    (*Cause examples to fail if LCF did*)

proof_timing := true;

(***  Section 10.4  ***)

-val ex_thy = extend_theory thy "Ex 10.4"
-([], [], [], [], [],
- [(["P"], "'a => tr"),
-  (["G","H"], "'a => 'a"),
-  (["K"], "('a => 'a) => ('a => 'a)")
- ],
- None)
-[ ("P_strict", "P(UU) = UU"),
-  ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
-  ("H", "H = FIX(K)")
-];
+val ex_thy =
+  thy
+   [("P", "'a => tr", NoSyn),
+    ("G", "'a => 'a", NoSyn),
+    ("H", "'a => 'a", NoSyn),
+    ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
+   [("P_strict", "P(UU) = UU"),
+    ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
+    ("H", "H = FIX(K)")]
+
val ax = get_axiom ex_thy;

val P_strict = ax"P_strict";
@@ -55,18 +57,20 @@

(***  Example 3.8  ***)

-val ex_thy = extend_theory thy "Ex 3.8"
-([], [], [], [], [],
- [(["P"], "'a => tr"),
-  (["F","G"], "'a => 'a"),
-  (["H"], "'a => 'b => 'b"),
-  (["K"], "('a => 'b => 'b) => ('a => 'b => 'b)")
- ],
- None)
-[ ("F_strict", "F(UU) = UU"),
-  ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
-  ("H", "H = FIX(K)")
-];
+val ex_thy =
+  thy
+   [("P", "'a => tr", NoSyn),
+    ("F", "'a => 'a", NoSyn),
+    ("G", "'a => 'a", NoSyn),
+    ("H", "'a => 'b => 'b", NoSyn),
+    ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
+   [("F_strict", "F(UU) = UU"),
+    ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
+    ("H", "H = FIX(K)")]
+
val ax = get_axiom ex_thy;

val F_strict = ax"F_strict";
@@ -85,15 +89,16 @@

(*** Addition with fixpoint of successor ***)

-val ex_thy = extend_theory thy "fix ex"
-([], [], [], [], [],
- [(["s"], "'a => 'a"),
-  (["p"], "'a => 'a => 'a")
- ],
- None)
-[ ("p_strict", "p(UU) = UU"),
-  ("p_s", "p(s(x),y) = s(p(x,y))")
-];
+val ex_thy =
+  thy