reactivated dead code;
authorwenzelm
Sat Jul 18 20:37:16 2015 +0200 (2015-07-18)
changeset 6075183f04804696c
parent 60750 7694aa52ad56
child 60752 b48830b670a1
reactivated dead code;
src/HOL/Bali/TypeSafe.thy
src/HOL/ROOT
     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)
     2.1 --- a/src/HOL/ROOT	Fri Jul 17 21:45:15 2015 +0200
     2.2 +++ b/src/HOL/ROOT	Sat Jul 18 20:37:16 2015 +0200
     2.3 @@ -467,6 +467,7 @@
     2.4      AxSound
     2.5      AxCompl
     2.6      Trans
     2.7 +    TypeSafe
     2.8    document_files "root.tex"
     2.9  
    2.10  session "HOL-IOA" in IOA = HOL +