# HG changeset patch
# User wenzelm
# Date 876739911 -7200
# Node ID e694c660055b7174cf8804448f7b6096c9a14199
# Parent  fe9932a7cd465e0a7dcf58829bcd59754051c67e
fixed dots;

diff -r fe9932a7cd46 -r e694c660055b src/HOLCF/IOA/ABP/Lemmas.ML
--- 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();
diff -r fe9932a7cd46 -r e694c660055b src/HOLCF/IOA/NTP/Impl.thy
--- 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 
diff -r fe9932a7cd46 -r e694c660055b src/HOLCF/IOA/NTP/Multiset.thy
--- 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)"
diff -r fe9932a7cd46 -r e694c660055b src/HOLCF/IOA/NTP/Receiver.thy
--- 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)                         &