src/HOL/IOA/ABP/Sender.thy
changeset 1476 608483c2122a
parent 1376 92f83b9d17e1
     1.1 --- a/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:27:16 1996 +0100
     1.2 +++ b/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:29:06 1996 +0100
     1.3 @@ -41,15 +41,15 @@
     1.4                    sbit(t)=sbit(s)  |                                 
     1.5        R_msg(m) => False |                                            
     1.6        S_pkt(pkt) => sq(s) ~= []  &                                   
     1.7 -		     hdr(pkt) = sbit(s)      &                        
     1.8 +                     hdr(pkt) = sbit(s)      &                        
     1.9                      msg(pkt) = hd(sq(s))    &                   
    1.10                      sq(t) = sq(s)           &                        
    1.11                      sbit(t) = sbit(s) |                              
    1.12        R_pkt(pkt) => False |                                          
    1.13        S_ack(b)   => False |                                          
    1.14        R_ack(b)   => if b = sbit(s) then                              
    1.15 -		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
    1.16 -		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    1.17 +                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
    1.18 +                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
    1.19  
    1.20  sender_ioa_def "sender_ioa == 
    1.21   (sender_asig, {([],True)}, sender_trans)"