src/HOL/Bali/TypeSafe.thy
changeset 32693 6c6b1ba5e71e
parent 28524 644b62cf678f
child 32960 69916a850301
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:14 2009 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:15 2009 +0200
     1.3 @@ -2953,7 +2953,7 @@
     1.4  	  by simp
     1.5  	from da_e1 s0_s1 True obtain E1' where
     1.6  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
     1.7 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
     1.8 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
     1.9  	with conf_s1 wt_e1
    1.10  	obtain 
    1.11  	  "s2\<Colon>\<preceq>(G, L)"
    1.12 @@ -2972,7 +2972,7 @@
    1.13  	  by simp
    1.14  	from da_e2 s0_s1 False obtain E2' where
    1.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    1.16 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    1.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
    1.18  	with conf_s1 wt_e2
    1.19  	obtain 
    1.20  	  "s2\<Colon>\<preceq>(G, L)"