Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
>0 -> ~=0
authornipkow
Mon, 22 Oct 2007 13:59:41 +0200
changeset 25141 8072027dc4bb
parent 25140 273772abbea2
child 25142 57c717b9dd59
>0 -> ~=0
src/HOLCF/IOA/NTP/Multiset.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle