# HG changeset patch
# User nipkow
# Date 1193054381 -7200
# Node ID 8072027dc4bbbb684d63cab8b4f05e8115e7eac3
# Parent  273772abbea274fbfb00165e92323b95893df985
>0 -> ~=0

diff -r 273772abbea2 -r 8072027dc4bb src/HOLCF/IOA/NTP/Multiset.thy
--- 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)