Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Bali/TypeSafe.thy
changeset 54859 64ff7f16d5b7
parent 52037 837211662fb8
child 55417 01fbfb60c33e 
--- a/src/HOL/Bali/TypeSafe.thy	Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Dec 25 15:52:25 2013 +0100
@@ -2946,7 +2946,7 @@
           by simp
         from da_e1 s0_s1 True obtain E1' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e1
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
@@ -2965,7 +2965,7 @@
           by simp
         from da_e2 s0_s1 False obtain E2' where
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
-          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
+          by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
         with conf_s1 wt_e2
         obtain 
           "s2\<Colon>\<preceq>(G, L)"
isabelle