--- a/src/HOLCF/ex/Fix2.thy Sun May 28 19:54:20 2006 +0200
+++ b/src/HOLCF/ex/Fix2.thy Sun May 28 20:53:03 2006 +0200
@@ -17,6 +17,19 @@
gix1_def: "F$(gix$F) = gix$F"
gix2_def: "F$y=y ==> gix$F << y"
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemma lemma1: "fix = gix"
+apply (rule ext_cfun)
+apply (rule antisym_less)
+apply (rule fix_least)
+apply (rule gix1_def)
+apply (rule gix2_def)
+apply (rule fix_eq [symmetric])
+done
+
+lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
+apply (rule lemma1 [THEN subst])
+apply (rule fix_def2)
+done
end