| changeset 25161 | aa8474398030 |
| parent 25113 | 008c964dd47f |
| child 26305 | 651371f29e00 |
--- a/src/HOLCF/IOA/NTP/Impl.thy Tue Oct 23 14:00:06 2007 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Tue Oct 23 22:48:25 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 neq0_conv split add: split_if) + Multiset.delm_nonempty_def split add: split_if) apply (rule allI) apply (rule conjI) apply (rule impI)