--- 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>"