src/HOL/Bali/Evaln.thy
changeset 13601 fd3e3d6b37b2
parent 13462 56610e2ba220
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/Evaln.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -600,7 +600,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      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
    1.11        by blast
    1.12 @@ -1558,7 +1558,7 @@
    1.13                   mode: "mode = invmode statM e" and
    1.14                      T: "T =Inl (resTy statM)" and
    1.15          eq_accC_accC': "accC=accC'"
    1.16 -      by (rule wt_elim_cases) auto
    1.17 +      by (rule wt_elim_cases) fastsimp+
    1.18      from conf_s0 wt_e
    1.19      obtain n1 where
    1.20        evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
    1.21 @@ -1793,7 +1793,7 @@
    1.22                  stat: "stat=is_static f" and
    1.23                 accC': "accC'=accC" and
    1.24  	           T: "T=(Inl (type f))"
    1.25 -       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
    1.26 +       by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
    1.27      from wf wt_e 
    1.28      have iscls_statC: "is_class G statC"
    1.29        by (auto dest: ty_expr_is_type type_is_class)