src/HOLCF/IOA/NTP/Impl.thy
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