src/HOL/Bali/Evaln.thy
 changeset 44890 22f665a2e91c parent 39159 0dec18004e75 child 46714 a7ca72710dfe
```     1.1 --- a/src/HOL/Bali/Evaln.thy	Sun Sep 11 22:56:05 2011 +0200
1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Sep 12 07:55:43 2011 +0200
1.3 @@ -305,7 +305,7 @@
1.4      then have "False" by induct auto
1.5    }
1.6    then show ?thesis
1.7 -    by (cases s') fastsimp
1.8 +    by (cases s') fastforce
1.9  qed
1.10
1.11  lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
1.12 @@ -317,7 +317,7 @@
1.13      then have "False" by induct auto
1.14    }
1.15    then show ?thesis
1.16 -    by (cases s') fastsimp
1.17 +    by (cases s') fastforce
1.18  qed
1.19
1.20  lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
1.21 @@ -329,7 +329,7 @@
1.22      then have "False" by induct auto
1.23    }
1.24    then show ?thesis
1.25 -    by (cases s') fastsimp
1.26 +    by (cases s') fastforce
1.27  qed
1.28
1.29  lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
1.30 @@ -341,7 +341,7 @@
1.31      then have "False" by induct auto
1.32    }
1.33    then show ?thesis
1.34 -    by (cases s') fastsimp
1.35 +    by (cases s') fastforce
1.36  qed
1.37
1.38  lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow>
1.39 @@ -602,7 +602,7 @@
1.40    moreover
1.41    from Try.hyps obtain n2 where
1.42      "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
1.43 -    by fastsimp
1.44 +    by fastforce
1.45    ultimately
1.46    have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
1.47      by (auto intro!: evaln.Try le_maxI1 le_maxI2)
```