# HG changeset patch
# User wenzelm
# Date 1192981691 -7200
# Node ID 3cfa2a60837fca6635d016a7e54d4ea6c746988b
# Parent  4f8176c940cfb46312a3be410d20884aa86629b1
fixed proof: neq0_conv;

diff -r 4f8176c940cf -r 3cfa2a60837f src/HOLCF/IOA/NTP/Multiset.thy
--- 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