rule swap: renamed Pa to P;
authorwenzelm
Wed, 26 Mar 2008 22:40:09 +0100
changeset 26417 af821e3a99e1
parent 26416 a66f86ef7bb9
child 26418 02709831944a
rule swap: renamed Pa to P;
src/ZF/Induct/Multiset.thy
--- 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}) ")