diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Receiver.thy
--- a/IOA/example/Receiver.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Receiver.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Receiver = List + IOA + Action + Multiset + "Lemmas" +
+(*  Title:      HOL/IOA/example/Receiver.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The implementation: receiver
+*)
+
+Receiver = List + IOA + Action + Multiset +
 
 types 
 
@@ -17,7 +25,7 @@
   rbit          :: "'m receiver_state => bool"
   rsending      :: "'m receiver_state => bool"
 
-rules
+defs
 
 rq_def       "rq == fst"
 rsent_def    "rsent == fst o snd"
@@ -25,9 +33,9 @@
 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)}),                          \
+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 ==                                    \
@@ -55,7 +63,7 @@
 \                     rbit(t)=rbit(s)                    &               \
 \                     rsending(s)                        &               \
 \                     rsending(t) |                                      \
-\R_ack(b) => False |                                                  \
+\      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)                        &                     \