--- a/src/HOL/Proofs/Lambda/ParRed.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Proofs/Lambda/ParRed.thy Mon Sep 12 07:55:43 2011 +0200
@@ -58,7 +58,7 @@
lemma par_beta_lift [simp]:
"t => t' \<Longrightarrow> lift t n => lift t' n"
- by (induct t arbitrary: t' n) fastsimp+
+ by (induct t arbitrary: t' n) fastforce+
lemma par_beta_subst:
"s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
@@ -67,8 +67,8 @@
apply (erule par_beta_cases)
apply simp
apply (simp add: subst_subst [symmetric])
- apply (fastsimp intro!: par_beta_lift)
- apply fastsimp
+ apply (fastforce intro!: par_beta_lift)
+ apply fastforce
done