# HG changeset patch
# User wenzelm
# Date 1437244636 -7200
# Node ID 83f04804696cc1aca327a1e78399f1a0f82e31da
# Parent  7694aa52ad56f0f83774894ba11e6992900de3a9
reactivated dead code;

diff -r 7694aa52ad56 -r 83f04804696c src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Fri Jul 17 21:45:15 2015 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Sat Jul 18 20:37:16 2015 +0200
@@ -3889,7 +3889,7 @@
 proof -
   note inj_term_simps [simp]
   from eval 
-  show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
+  have "\<And>L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
                        \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
         \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
   proof (induct)
diff -r 7694aa52ad56 -r 83f04804696c src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jul 17 21:45:15 2015 +0200
+++ b/src/HOL/ROOT	Sat Jul 18 20:37:16 2015 +0200
@@ -467,6 +467,7 @@
     AxSound
     AxCompl
     Trans
+    TypeSafe
   document_files "root.tex"
 
 session "HOL-IOA" in IOA = HOL +