src/HOL/Bali/TypeSafe.thy
changeset 13601 fd3e3d6b37b2
parent 13384 a34e38154413
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -1895,7 +1895,7 @@
     1.4                   mode: "mode = invmode statM e" and
     1.5                      T: "T =Inl (resTy statM)" and
     1.6          eq_accC_accC': "accC=accC'"
     1.7 -      by (rule wt_elim_cases) auto
     1.8 +      by (rule wt_elim_cases) fastsimp+
     1.9      from conf_s0 wt_e hyp_e 
    1.10      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
    1.11             conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
    1.12 @@ -1947,7 +1947,7 @@
    1.13  	by auto
    1.14        ultimately have
    1.15  	"set_lvars (locals (store s2)) s4 = s2"
    1.16 -	by (cases s2,cases s4) (simp add: init_lvars_def2)
    1.17 +	by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
    1.18        with False conf_s2 error_free_s2
    1.19        show ?thesis
    1.20  	by auto
    1.21 @@ -1981,7 +1981,7 @@
    1.22  	ultimately have
    1.23  	  "set_lvars (locals (store s2)) s4 
    1.24             = (Some (Xcpt (Std NullPointer)),store s2)"
    1.25 -	  by (cases s2,cases s4) (simp add: init_lvars_def2)
    1.26 +	  by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
    1.27  	with conf_s2 error_free_s2
    1.28  	show ?thesis
    1.29  	  by (cases s2) (auto dest: conforms_NormI)