--- a/src/HOLCF/IOA/ABP/Lemmas.ML Mon Oct 13 12:48:42 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Mon Oct 13 12:51:51 1997 +0200
@@ -31,7 +31,7 @@
(* 2 Lemmas to add to set_lemmas ... , used also for action handling,
namely for Intersections and the empty list (compatibility of IOA!) *)
-goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})";
+goal Set.thy "(UN b.{x. x=f(b)})= (UN b.{f(b)})";
by (rtac set_ext 1);
by (Fast_tac 1);
val singleton_set =result();
--- 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
--- a/src/HOLCF/IOA/NTP/Multiset.thy Mon Oct 13 12:48:42 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Mon Oct 13 12:51:51 1997 +0200
@@ -40,7 +40,7 @@
"countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
count_def
- "count M x == countm M (%y.y = x)"
+ "count M x == countm M (%y. y = x)"
induction
"[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
--- a/src/HOLCF/IOA/NTP/Receiver.thy Mon Oct 13 12:48:42 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Receiver.thy Mon Oct 13 12:51:51 1997 +0200
@@ -65,7 +65,7 @@
rsending(t) |
R_ack(b) => False |
C_m_s => False |
- C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
rq(t) = rq(s) &
rsent(t)=rsent(s) &
rrcvd(t)=rrcvd(s) &
@@ -73,7 +73,7 @@
rsending(s) &
~rsending(t) |
C_r_s => False |
- C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
rq(t) = rq(s)@[m] &
rsent(t)=rsent(s) &