--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/ex/Ex1.thy	Fri May 08 13:54:45 1998 +0200
@@ -0,0 +1,17 @@
+
+(***  Section 10.4  ***)
+
+Ex1 = LCF +
+
+consts
+  P	:: "'a => tr"
+  G	:: "'a => 'a"
+  H	:: "'a => 'a"
+  K	:: "('a => 'a) => ('a => 'a)"
+
+rules
+  P_strict	"P(UU) = UU"
+  K		"K = (%h x. P(x) => x | h(h(G(x))))"
+  H		"H = FIX(K)"
+
+end