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.
fixed proof: neq0_conv;
authorwenzelm
Sun, 21 Oct 2007 17:48:11 +0200
changeset 25136 3cfa2a60837f
parent 25135 4f8176c940cf
child 25137 0835ac64834a
fixed proof: neq0_conv;
src/HOLCF/IOA/NTP/Multiset.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IOA/NTP/Multiset.thy	Sun Oct 21 16:27:42 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy	Sun Oct 21 17:48:11 2007 +0200
@@ -85,7 +85,7 @@
    "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"
   apply (rule_tac M = "M" in Multiset.induction)
   apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
-  apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
+  apply (simp (no_asm_simp) add: neq0_conv count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
   apply auto
   done
isabelle