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