author | wenzelm |
Wed, 26 Mar 2008 22:40:09 +0100 | |
changeset 26417 | af821e3a99e1 |
parent 26416 | a66f86ef7bb9 |
child 26418 | 02709831944a |
--- a/src/ZF/Induct/Multiset.thy Wed Mar 26 22:40:08 2008 +0100 +++ b/src/ZF/Induct/Multiset.thy Wed Mar 26 22:40:09 2008 +0100 @@ -364,7 +364,7 @@ lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 <-> M=0" apply (simp add: msize_def, auto) -apply (rule_tac Pa = "setsum (?u,?v) \<noteq> #0" in swap) +apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap) apply blast apply (drule not_empty_multiset_imp_exist, assumption, clarify) apply (subgoal_tac "Finite (mset_of (M) - {a}) ")