diff -r c3913a79b6ae -r 492493334e0f IOA/example/Sender.thy
--- a/IOA/example/Sender.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Sender.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -32,54 +32,54 @@
 ssending_def "ssending == snd o snd o snd o snd"
 
 sender_asig_def
-  "sender_asig == <(UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       \
-\                  UN pkt. {S_pkt(pkt)},                           \
-\                  {C_m_s,C_r_s}>"
+  "sender_asig == <(UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
+                  UN pkt. {S_pkt(pkt)},                           
+                  {C_m_s,C_r_s}>"
 
-sender_trans_def "sender_trans ==                                     \
-\ {tr. let s = fst(tr);                                               \
-\          t = snd(snd(tr))                                           \
-\      in case fst(snd(tr))                                           \
-\      of                                                             \
-\      S_msg(m) => sq(t)=sq(s)@[m]   &                                \
-\                  ssent(t)=ssent(s) &                                \
-\                  srcvd(t)=srcvd(s) &                                \
-\                  sbit(t)=sbit(s)   &                                \
-\                  ssending(t)=ssending(s) |                          \
-\      R_msg(m) => False |                                            \
-\      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                     \
-\                       (? Q. sq(s) = (msg(pkt)#Q))  &               \
-\                       sq(t) = sq(s)           &                     \
-\                       ssent(t) = addm(ssent(s),sbit(s)) &           \
-\                       srcvd(t) = srcvd(s) &                         \
-\                       sbit(t) = sbit(s)   &                         \
-\                       ssending(s)         &                         \
-\                       ssending(t) |                                 \
-\    R_pkt(pkt) => False |                                         \
-\    S_ack(b)   => False |                                         \
-\      R_ack(b) => sq(t)=sq(s)                  &                  \
-\                     ssent(t)=ssent(s)            &                  \
-\                     srcvd(t) = addm(srcvd(s),b)  &                  \
-\                     sbit(t)=sbit(s)              &                  \
-\                     ssending(t)=ssending(s) |                       \
-\      C_m_s => count(ssent(s),~sbit(s)) < count(srcvd(s),~sbit(s)) & \
-\               sq(t)=sq(s)       &                                   \
-\               ssent(t)=ssent(s) &                                   \
-\               srcvd(t)=srcvd(s) &                                   \
-\               sbit(t)=sbit(s)   &                                   \
-\               ssending(s)       &                                   \
-\               ~ssending(t) |                                        \
-\      C_m_r => False |                                               \
-\      C_r_s => count(ssent(s),sbit(s)) <= count(srcvd(s),~sbit(s)) & \
-\               sq(t)=tl(sq(s))      &                                \
-\               ssent(t)=ssent(s)    &                                \
-\               srcvd(t)=srcvd(s)    &                                \
-\               sbit(t) = (~sbit(s)) &                                \
-\               ~ssending(s)         &                                \
-\               ssending(t) |                                         \
-\      C_r_r(m) => False}"
+sender_trans_def "sender_trans ==                                     
+ {tr. let s = fst(tr);                                               
+          t = snd(snd(tr))                                           
+      in case fst(snd(tr))                                           
+      of                                                             
+      S_msg(m) => sq(t)=sq(s)@[m]   &                                
+                  ssent(t)=ssent(s) &                                
+                  srcvd(t)=srcvd(s) &                                
+                  sbit(t)=sbit(s)   &                                
+                  ssending(t)=ssending(s) |                          
+      R_msg(m) => False |                                            
+      S_pkt(pkt) => hdr(pkt) = sbit(s)      &                     
+                       (? Q. sq(s) = (msg(pkt)#Q))  &               
+                       sq(t) = sq(s)           &                     
+                       ssent(t) = addm(ssent(s),sbit(s)) &           
+                       srcvd(t) = srcvd(s) &                         
+                       sbit(t) = sbit(s)   &                         
+                       ssending(s)         &                         
+                       ssending(t) |                                 
+    R_pkt(pkt) => False |                                         
+    S_ack(b)   => False |                                         
+      R_ack(b) => sq(t)=sq(s)                  &                  
+                     ssent(t)=ssent(s)            &                  
+                     srcvd(t) = addm(srcvd(s),b)  &                  
+                     sbit(t)=sbit(s)              &                  
+                     ssending(t)=ssending(s) |                       
+      C_m_s => count(ssent(s),~sbit(s)) < count(srcvd(s),~sbit(s)) & 
+               sq(t)=sq(s)       &                                   
+               ssent(t)=ssent(s) &                                   
+               srcvd(t)=srcvd(s) &                                   
+               sbit(t)=sbit(s)   &                                   
+               ssending(s)       &                                   
+               ~ssending(t) |                                        
+      C_m_r => False |                                               
+      C_r_s => count(ssent(s),sbit(s)) <= count(srcvd(s),~sbit(s)) & 
+               sq(t)=tl(sq(s))      &                                
+               ssent(t)=ssent(s)    &                                
+               srcvd(t)=srcvd(s)    &                                
+               sbit(t) = (~sbit(s)) &                                
+               ~ssending(s)         &                                
+               ssending(t) |                                         
+      C_r_r(m) => False}"
 
-sender_ioa_def "sender_ioa == \
-\ <sender_asig, {<[],{|},{|},False,True>}, sender_trans>"
+sender_ioa_def "sender_ioa == 
+ <sender_asig, {<[],{|},{|},False,True>}, sender_trans>"
 
 end