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)