ProgTutorial/Package/Ind_Prelims.thy
changeset 513 f223f8223d4a
parent 346 0fea8b7a14a1
child 562 daf404920ab9
--- 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])