diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOLCF/IOA/NTP/Receiver.thy	Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Receiver.thy	Sat Sep 03 16:50:22 2005 +0200
@@ -1,13 +1,15 @@
 (*  Title:      HOL/IOA/NTP/Receiver.thy
     ID:         $Id$
     Author:     Tobias Nipkow & Konrad Slind
-
-The implementation: receiver.
 *)
 
-Receiver = List + IOA + Action + 
+header {* The implementation: receiver *}
 
-types 
+theory Receiver
+imports IOA Action
+begin
+
+types
 
 'm receiver_state
 = "'m list * bool multiset * 'm packet multiset * bool * bool"
@@ -16,73 +18,75 @@
 consts
 
   receiver_asig :: "'m action signature"
-  receiver_trans:: ('m action, 'm receiver_state)transition set
-  receiver_ioa  :: ('m action, 'm receiver_state)ioa
-  rq            :: 'm receiver_state => 'm list
-  rsent         :: 'm receiver_state => bool multiset
-  rrcvd         :: 'm receiver_state => 'm packet multiset
-  rbit          :: 'm receiver_state => bool
-  rsending      :: 'm receiver_state => bool
+  receiver_trans:: "('m action, 'm receiver_state)transition set"
+  receiver_ioa  :: "('m action, 'm receiver_state)ioa"
+  rq            :: "'m receiver_state => 'm list"
+  rsent         :: "'m receiver_state => bool multiset"
+  rrcvd         :: "'m receiver_state => 'm packet multiset"
+  rbit          :: "'m receiver_state => bool"
+  rsending      :: "'m receiver_state => bool"
 
 defs
 
-rq_def       "rq == fst"
-rsent_def    "rsent == fst o snd"
-rrcvd_def    "rrcvd == fst o snd o snd"
-rbit_def     "rbit == fst o snd o snd o snd"
-rsending_def "rsending == snd o snd o snd o snd"
+rq_def:       "rq == fst"
+rsent_def:    "rsent == fst o snd"
+rrcvd_def:    "rrcvd == fst o snd o snd"
+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 ==                                    
- {tr. let s = fst(tr);                                                  
-          t = snd(snd(tr))                                              
-      in                                                                
-      case fst(snd(tr))                                                 
-      of                                                                
-      S_msg(m) => False |                                               
-      R_msg(m) => rq(s) = (m # rq(t))   &                               
-                  rsent(t)=rsent(s)     &                               
-                  rrcvd(t)=rrcvd(s)     &                               
-                  rbit(t)=rbit(s)       &                               
-                  rsending(t)=rsending(s) |                             
-      S_pkt(pkt) => False |                                          
-      R_pkt(pkt) => rq(t) = rq(s)                        &           
-                       rsent(t) = rsent(s)                  &           
-                       rrcvd(t) = addm (rrcvd s) pkt        &           
-                       rbit(t) = rbit(s)                    &           
-                       rsending(t) = rsending(s) |                      
-      S_ack(b) => b = rbit(s)                        &               
-                     rq(t) = rq(s)                      &               
-                     rsent(t) = addm (rsent s) (rbit s) &               
-                     rrcvd(t) = rrcvd(s)                &               
-                     rbit(t)=rbit(s)                    &               
-                     rsending(s)                        &               
-                     rsending(t) |                                      
-      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)                        &                     
-             rsent(t)=rsent(s)                    &                     
-             rrcvd(t)=rrcvd(s)                    &                     
-             rbit(t)=rbit(s)                      &                     
-             rsending(s)                          &                     
-             ~rsending(t) |                                             
-    C_r_s => False |                                                    
- C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) & 
-             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &  
-             rq(t) = rq(s)@[m]                         &                
-             rsent(t)=rsent(s)                         &                
-             rrcvd(t)=rrcvd(s)                         &                
-             rbit(t) = (~rbit(s))                      &                
-             ~rsending(s)                              &                
+receiver_trans_def: "receiver_trans ==
+ {tr. let s = fst(tr);
+          t = snd(snd(tr))
+      in
+      case fst(snd(tr))
+      of
+      S_msg(m) => False |
+      R_msg(m) => rq(s) = (m # rq(t))   &
+                  rsent(t)=rsent(s)     &
+                  rrcvd(t)=rrcvd(s)     &
+                  rbit(t)=rbit(s)       &
+                  rsending(t)=rsending(s) |
+      S_pkt(pkt) => False |
+      R_pkt(pkt) => rq(t) = rq(s)                        &
+                       rsent(t) = rsent(s)                  &
+                       rrcvd(t) = addm (rrcvd s) pkt        &
+                       rbit(t) = rbit(s)                    &
+                       rsending(t) = rsending(s) |
+      S_ack(b) => b = rbit(s)                        &
+                     rq(t) = rq(s)                      &
+                     rsent(t) = addm (rsent s) (rbit s) &
+                     rrcvd(t) = rrcvd(s)                &
+                     rbit(t)=rbit(s)                    &
+                     rsending(s)                        &
+                     rsending(t) |
+      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)                        &
+             rsent(t)=rsent(s)                    &
+             rrcvd(t)=rrcvd(s)                    &
+             rbit(t)=rbit(s)                      &
+             rsending(s)                          &
+             ~rsending(t) |
+    C_r_s => False |
+ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
+             count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
+             rq(t) = rq(s)@[m]                         &
+             rsent(t)=rsent(s)                         &
+             rrcvd(t)=rrcvd(s)                         &
+             rbit(t) = (~rbit(s))                      &
+             ~rsending(s)                              &
              rsending(t)}"
 
 
-receiver_ioa_def "receiver_ioa == 
+receiver_ioa_def: "receiver_ioa ==
  (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end