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)"
```