# HG changeset patch
# User wenzelm
# Date 1206567609 -3600
# Node ID af821e3a99e105ca8f7bbd643cc3e5a2830d4dca
# Parent  a66f86ef7bb97e19e7d456d9f9ef0ebd90a29208
rule swap: renamed Pa to P;

diff -r a66f86ef7bb9 -r af821e3a99e1 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}) ")