src/HOL/Bali/DefiniteAssignmentCorrect.thy
changeset 13811 f39f67982854
parent 13690 ac335b2f4a39
child 14030 cd928c0ac225
     1.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Feb 07 16:40:23 2003 +0100
     1.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Feb 08 14:46:22 2003 +0100
     1.3 @@ -2247,7 +2247,7 @@
     1.4  proof -
     1.5    -- {* To properly perform induction on the evaluation relation we have to
     1.6          generalize the lemma to terms not only expressions. *}
     1.7 -  {fix t val
     1.8 +  { fix t val
     1.9     assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
    1.10     assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
    1.11     assume expr:  "\<exists> expr. t=In1l expr"
    1.12 @@ -3634,7 +3634,7 @@
    1.13          hence "normal s2"
    1.14            by (cases s2) simp
    1.15          with nrmAss_A' nrm_A_A' s2_s3 show ?thesis
    1.16 -          by auto
    1.17 +          by blast
    1.18        qed
    1.19      qed
    1.20      moreover