Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reactivated dead code;
authorwenzelm
Sat, 18 Jul 2015 20:37:16 +0200
changeset 60751 83f04804696c
parent 60750 7694aa52ad56
child 60752 b48830b670a1
reactivated dead code;
src/HOL/Bali/TypeSafe.thy file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- 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)
--- 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 +
isabelle