diff -r c3913a79b6ae -r 492493334e0f IOA/example/Channels.thy
--- a/IOA/example/Channels.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Channels.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -21,46 +21,46 @@
 
 defs
 
-srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    \
-\                            UN pkt. {R_pkt(pkt)},    \
-\                            {}>"
+srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    
+                            UN pkt. {R_pkt(pkt)},    
+                            {}>"
 
-rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \
-\                            UN b. {R_ack(b)}, \
-\                            {}>"
+rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, 
+                            UN b. {R_ack(b)}, 
+                            {}>"
 
-srch_trans_def "srch_trans ==                                       \
-\ {tr. let s = fst(tr);                                             \
-\          t = snd(snd(tr))                                         \
-\      in                                                           \
-\      case fst(snd(tr))                                            \
-\        of S_msg(m) => False |                                     \
-\           R_msg(m) => False |                                     \
-\           S_pkt(pkt) => t = addm(s, pkt) |                        \
-\           R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) |   \
-\           S_ack(b) => False |                                     \
-\           R_ack(b) => False |                                     \
-\           C_m_s => False |                                        \
-\           C_m_r => False |                                        \
-\           C_r_s => False |                                        \
-\           C_r_r(m) => False}"
+srch_trans_def "srch_trans ==                                       
+ {tr. let s = fst(tr);                                             
+          t = snd(snd(tr))                                         
+      in                                                           
+      case fst(snd(tr))                                            
+        of S_msg(m) => False |                                     
+           R_msg(m) => False |                                     
+           S_pkt(pkt) => t = addm(s, pkt) |                        
+           R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) |   
+           S_ack(b) => False |                                     
+           R_ack(b) => False |                                     
+           C_m_s => False |                                        
+           C_m_r => False |                                        
+           C_r_s => False |                                        
+           C_r_r(m) => False}"
 
-rsch_trans_def "rsch_trans ==                         \
-\ {tr. let s = fst(tr);                               \
-\          t = snd(snd(tr))                           \
-\      in                                             \
-\      case fst(snd(tr))                              \
-\      of                                             \
-\      S_msg(m) => False |                            \
-\      R_msg(m) => False |                            \
-\      S_pkt(pkt) => False |                          \
-\      R_pkt(pkt) => False |                          \
-\      S_ack(b) => t = addm(s,b) |                    \
-\      R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) |  \
-\      C_m_s => False |                               \
-\      C_m_r => False |                               \
-\      C_r_s => False |                               \
-\      C_r_r(m) => False}"
+rsch_trans_def "rsch_trans ==                         
+ {tr. let s = fst(tr);                               
+          t = snd(snd(tr))                           
+      in                                             
+      case fst(snd(tr))                              
+      of                                             
+      S_msg(m) => False |                            
+      R_msg(m) => False |                            
+      S_pkt(pkt) => False |                          
+      R_pkt(pkt) => False |                          
+      S_ack(b) => t = addm(s,b) |                    
+      R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) |  
+      C_m_s => False |                               
+      C_m_r => False |                               
+      C_r_s => False |                               
+      C_r_r(m) => False}"
 
 
 srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"