--- a/src/HOLCF/IOA/NTP/Multiset.thy Sun Oct 21 22:33:35 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Mon Oct 22 13:59:41 2007 +0200
@@ -75,7 +75,7 @@
done
-lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> 0<countm M P"
+lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P \<noteq> 0"
apply (rule_tac M = "M" in Multiset.induction)
apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def)
apply (simp (no_asm_simp) add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)