changeset 3852 | e694c660055b |
parent 3073 | 88366253a09a |
child 12218 | 6597093b77e7 |
--- a/src/HOLCF/IOA/NTP/Impl.thy Mon Oct 13 12:48:42 1997 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Mon Oct 13 12:51:51 1997 +0200 @@ -36,7 +36,7 @@ rsch_def "rsch == snd o snd o snd" hdr_sum_def - "hdr_sum M b == countm M (%pkt.hdr(pkt) = b)" + "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" (* Lemma 5.1 *) inv1_def