author | wenzelm |
Sat, 20 Oct 2007 15:46:04 +0200 | |
changeset 25113 | 008c964dd47f |
parent 25112 | 98824cc791c0 |
child 25114 | 7aa178165ee4 |
--- 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)