# HG changeset patch
# User wenzelm
# Date 1192887964 -7200
# Node ID 008c964dd47f5cfd07d2e757ef978be465b915eb
# Parent  98824cc791c02ada0f6996e42c531715fbb144e9
fixed proof: neq0_conv;

diff -r 98824cc791c0 -r 008c964dd47f src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Sat Oct 20 12:09:33 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Sat Oct 20 15:46:04 2007 +0200
@@ -168,7 +168,7 @@
 apply (rule impI)
 apply (erule conjE)+
 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
-  Multiset.delm_nonempty_def split add: split_if)
+  Multiset.delm_nonempty_def neq0_conv split add: split_if)
 apply (rule allI)
 apply (rule conjI)
 apply (rule impI)