src/HOL/Bali/TypeSafe.thy
changeset 60751 83f04804696c
parent 58887 38db8ddc0f57
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Jul 17 21:45:15 2015 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sat Jul 18 20:37:16 2015 +0200
     1.3 @@ -3889,7 +3889,7 @@
     1.4  proof -
     1.5    note inj_term_simps [simp]
     1.6    from eval 
     1.7 -  show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
     1.8 +  have "\<And>L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
     1.9                         \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
    1.10          \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
    1.11    proof (induct)