src/HOL/Bali/TypeSafe.thy
changeset 15102 04b0e943fcc9
parent 14981 e73f8140af78
child 15217 15fa818ef624
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Aug 02 16:06:13 2004 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Aug 03 13:48:00 2004 +0200
     1.3 @@ -1477,7 +1477,7 @@
     1.4    qed
     1.5  next
     1.6    show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
     1.7 -  proof 
     1.8 +  proof (rule subsetI)
     1.9      fix el 
    1.10      assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
    1.11      show "el \<in> ?List x xs y ys"
    1.12 @@ -2978,7 +2978,7 @@
    1.13  	  by simp
    1.14  	from da_e1 s0_s1 True obtain E1' where
    1.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
    1.16 -	  by - (rule da_weakenE,auto)
    1.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    1.18  	with conf_s1 wt_e1
    1.19  	obtain 
    1.20  	  "s2\<Colon>\<preceq>(G, L)"
    1.21 @@ -2997,7 +2997,7 @@
    1.22  	  by simp
    1.23  	from da_e2 s0_s1 False obtain E2' where
    1.24  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    1.25 -	  by - (rule da_weakenE,auto)
    1.26 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    1.27  	with conf_s1 wt_e2
    1.28  	obtain 
    1.29  	  "s2\<Colon>\<preceq>(G, L)"