--- a/src/HOL/IMP/Types.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Types.thy Mon Sep 12 07:55:43 2011 +0200
@@ -120,7 +120,7 @@
lemma apreservation:
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
apply(induct arbitrary: v rule: atyping.induct)
-apply (fastsimp simp: styping_def)+
+apply (fastforce simp: styping_def)+
done
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
@@ -131,11 +131,11 @@
proof (cases v1)
case Iv
with Plus_ty(1,3,5) v show ?thesis
- by(fastsimp intro: taval.intros(4) dest!: apreservation)
+ by(fastforce intro: taval.intros(4) dest!: apreservation)
next
case Rv
with Plus_ty(1,3,5) v show ?thesis
- by(fastsimp intro: taval.intros(5) dest!: apreservation)
+ by(fastforce intro: taval.intros(5) dest!: apreservation)
qed
qed (auto intro: taval.intros)
@@ -148,11 +148,11 @@
proof (cases v1)
case Iv
with Less_ty v show ?thesis
- by (fastsimp intro!: tbval.intros(4) dest!:apreservation)
+ by (fastforce intro!: tbval.intros(4) dest!:apreservation)
next
case Rv
with Less_ty v show ?thesis
- by (fastsimp intro!: tbval.intros(5) dest!:apreservation)
+ by (fastforce intro!: tbval.intros(5) dest!:apreservation)
qed
qed (auto intro: tbval.intros)