src/LCF/ex/Ex3.thy

--- a/src/LCF/ex/Ex3.thy	Thu Jun 01 14:54:44 2006 +0200
+++ b/src/LCF/ex/Ex3.thy	Thu Jun 01 21:14:05 2006 +0200
@@ -15,6 +15,12 @@
   p_strict:     "p(UU) = UU"
   p_s:          "p(s(x),y) = s(p(x,y))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+declare p_strict [simp] p_s [simp]
+
+lemma example: "p(FIX(s),y) = FIX(s)"
+  apply (tactic {* induct_tac "s" 1 *})
+  apply (simp (no_asm))
+  apply (simp (no_asm))
+  done
 
 end