--- a/src/LCF/ex/Ex2.thy Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex2.thy Thu Jun 01 21:14:05 2006 +0200
@@ -19,6 +19,13 @@
K: "K = (%h x y. P(x) => y | F(h(G(x),y)))"
H: "H = FIX(K)"
-ML {* use_legacy_bindings (the_context ()) *}
+declare F_strict [simp] K [simp]
+
+lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
+ apply (simplesubst H)
+ apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+ apply (simp (no_asm))
+ apply (simp (no_asm_simp) split: COND_cases_iff)
+ done
end