diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Channels.thy
--- a/IOA/example/Channels.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Channels.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Channels = IOA + Action + Multiset + "Lemmas" + Packet +
+(*  Title:      HOL/IOA/example/Channels.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The (faulty) transmission channels (both directions)
+*)
+
+Channels = IOA + Action + Multiset +
 
 consts
 
@@ -11,7 +19,7 @@
 srch_ioa   :: "('m action, 'm packet multiset)ioa"
 rsch_ioa   :: "('m action, bool multiset)ioa"
 
-rules
+defs
 
 srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    \
 \                            UN pkt. {R_pkt(pkt)},    \
@@ -21,37 +29,37 @@
 \                            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 |                                        \
+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_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 |                               \
+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_m_s => False |                               \
+\      C_m_r => False |                               \
+\      C_r_s => False |                               \
 \      C_r_r(m) => False}"