# HG changeset patch
# User nipkow
# Date 1245435748 -7200
# Node ID b03270a8c23f5b2d20a46c933dc7b9425c32bb32
# Parent  29f5b20e8ee86504b3b91fc96761ad82b99b2ff8
tuned

diff -r 29f5b20e8ee8 -r b03270a8c23f src/HOL/NewNumberTheory/MiscAlgebra.thy
--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 18:33:10 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 20:22:28 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)