
diff -r 04e51b7a3422 -r 0e018cbcc0de src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 20:24:48 2011 +0200
@@ -85,16 +85,14 @@
 
 lemma LeadsTo_UN: 
      "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
-apply (simp only: Union_image_eq [symmetric])
+apply (unfold SUP_def)
 apply (blast intro: LeadsTo_Union)
 done
 
 text{*Binary union introduction rule*}
 lemma LeadsTo_Un:
      "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsTo_Union)
-done
+  using LeadsTo_UN [of "{A, B}" F id C] by auto
 
 text{*Lets us look at the starting state*}
 lemma single_LeadsTo_I:




