--- a/ProgTutorial/Package/Ind_Prelims.thy Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Package/Ind_Prelims.thy Sun Feb 19 01:33:47 2012 +0000
@@ -59,7 +59,7 @@
assumes "trcl R x y"
shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
apply(atomize (full))
-apply(cut_tac prems)
+apply(cut_tac assms)
apply(unfold trcl_def)
apply(drule spec[where x=P])
apply(assumption)
@@ -211,7 +211,7 @@
assumes "even n"
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
apply(atomize (full))
-apply(cut_tac prems)
+apply(cut_tac assms)
apply(unfold even_def)
apply(drule spec[where x=P])
apply(drule spec[where x=Q])