diff -r c3913a79b6ae -r 492493334e0f IOA/example/Receiver.thy
--- a/IOA/example/Receiver.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Receiver.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -33,57 +33,57 @@
 rbit_def     "rbit == fst o snd o snd o snd"
 rsending_def "rsending == snd o snd o snd o snd"
 
-receiver_asig_def "receiver_asig ==            \
-\ <UN pkt. {R_pkt(pkt)},                       \
-\  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   \
-\  insert(C_m_r, UN m. {C_r_r(m)})>"
+receiver_asig_def "receiver_asig ==            
+ <UN pkt. {R_pkt(pkt)},                       
+  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
+  insert(C_m_r, UN m. {C_r_r(m)})>"
 
-receiver_trans_def "receiver_trans ==                                    \
-\ {tr. let s = fst(tr);                                                  \
-\          t = snd(snd(tr))                                              \
-\      in                                                                \
-\      case fst(snd(tr))                                                 \
-\      of                                                                \
-\      S_msg(m) => False |                                               \
-\      R_msg(m) => rq(s) = (m # rq(t))   &                               \
-\                  rsent(t)=rsent(s)     &                               \
-\                  rrcvd(t)=rrcvd(s)     &                               \
-\                  rbit(t)=rbit(s)       &                               \
-\                  rsending(t)=rsending(s) |                             \
-\      S_pkt(pkt) => False |                                          \
-\      R_pkt(pkt) => rq(t) = rq(s)                        &           \
-\                       rsent(t) = rsent(s)                  &           \
-\                       rrcvd(t) = addm(rrcvd(s),pkt)        &           \
-\                       rbit(t) = rbit(s)                    &           \
-\                       rsending(t) = rsending(s) |                      \
-\      S_ack(b) => b = rbit(s)                        &               \
-\                     rq(t) = rq(s)                      &               \
-\                     rsent(t) = addm(rsent(s),rbit(s))  &               \
-\                     rrcvd(t) = rrcvd(s)                &               \
-\                     rbit(t)=rbit(s)                    &               \
-\                     rsending(s)                        &               \
-\                     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)) & \
-\             rq(t) = rq(s)                        &                     \
-\             rsent(t)=rsent(s)                    &                     \
-\             rrcvd(t)=rrcvd(s)                    &                     \
-\             rbit(t)=rbit(s)                      &                     \
-\             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)) & \
-\             count(rsent(s),~rbit(s)) < count(rrcvd(s),<rbit(s),m>) &   \
-\             rq(t) = rq(s)@[m]                         &                \
-\             rsent(t)=rsent(s)                         &                \
-\             rrcvd(t)=rrcvd(s)                         &                \
-\             rbit(t) = (~rbit(s))                      &                \
-\             ~rsending(s)                              &                \
-\             rsending(t)}"
+receiver_trans_def "receiver_trans ==                                    
+ {tr. let s = fst(tr);                                                  
+          t = snd(snd(tr))                                              
+      in                                                                
+      case fst(snd(tr))                                                 
+      of                                                                
+      S_msg(m) => False |                                               
+      R_msg(m) => rq(s) = (m # rq(t))   &                               
+                  rsent(t)=rsent(s)     &                               
+                  rrcvd(t)=rrcvd(s)     &                               
+                  rbit(t)=rbit(s)       &                               
+                  rsending(t)=rsending(s) |                             
+      S_pkt(pkt) => False |                                          
+      R_pkt(pkt) => rq(t) = rq(s)                        &           
+                       rsent(t) = rsent(s)                  &           
+                       rrcvd(t) = addm(rrcvd(s),pkt)        &           
+                       rbit(t) = rbit(s)                    &           
+                       rsending(t) = rsending(s) |                      
+      S_ack(b) => b = rbit(s)                        &               
+                     rq(t) = rq(s)                      &               
+                     rsent(t) = addm(rsent(s),rbit(s))  &               
+                     rrcvd(t) = rrcvd(s)                &               
+                     rbit(t)=rbit(s)                    &               
+                     rsending(s)                        &               
+                     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)) & 
+             rq(t) = rq(s)                        &                     
+             rsent(t)=rsent(s)                    &                     
+             rrcvd(t)=rrcvd(s)                    &                     
+             rbit(t)=rbit(s)                      &                     
+             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)) & 
+             count(rsent(s),~rbit(s)) < count(rrcvd(s),<rbit(s),m>) &   
+             rq(t) = rq(s)@[m]                         &                
+             rsent(t)=rsent(s)                         &                
+             rrcvd(t)=rrcvd(s)                         &                
+             rbit(t) = (~rbit(s))                      &                
+             ~rsending(s)                              &                
+             rsending(t)}"
 
 
-receiver_ioa_def "receiver_ioa == \
-\ <receiver_asig, {<[],{|},{|},False,False>}, receiver_trans>"
+receiver_ioa_def "receiver_ioa == 
+ <receiver_asig, {<[],{|},{|},False,False>}, receiver_trans>"
 
 end