| changeset 25113 | 008c964dd47f |
| parent 24327 | a207114007c6 |
| child 25161 | aa8474398030 |
--- 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)