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