# HG changeset patch
# User nipkow
# Date 1245435766 -7200
# Node ID caa89b41dcf267da5827495116c185e5d6222094
# Parent  d1ac3f3b2f54385a3af4475fa728199bfeb6409d# Parent  b03270a8c23f5b2d20a46c933dc7b9425c32bb32
merged

diff -r d1ac3f3b2f54 -r caa89b41dcf2 src/HOL/NewNumberTheory/MiscAlgebra.thy
--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 18:56:53 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 20:22:46 2009 +0200
@@ -45,12 +45,6 @@
 
 *)
 
-(* This could go in Set.thy *)
-
-lemma UNION_empty: "(UNION F A = {}) = (ALL x: F. (A x) = {})"
-  by auto
-
-
 (* The rest is for the algebra libraries *)
 
 (* This goes in FuncSet.thy. Any reason not to make it a simp rule? *)
@@ -293,11 +287,7 @@
   apply blast
   apply (erule finite_UN_I)
   apply blast
-  apply (subst Int_UN_distrib)
-  apply (subst UNION_empty)
-  apply clarsimp
-  apply (drule_tac x = xa in bspec)back
-  apply (assumption, force)
+  apply (fastsimp)
   apply (auto intro!: funcsetI finprod_closed) 
   apply (subst finprod_insert)
   apply (auto intro!: funcsetI finprod_closed)