1.1 --- a/src/HOLCF/IOA/NTP/Spec.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,40 +0,0 @@
     1.4 -(*  Title:      HOL/IOA/NTP/Spec.thy
     1.5 -    Author:     Tobias Nipkow & Konrad Slind
     1.6 -*)
     1.7 -
     1.8 -header {* The specification of reliable transmission *}
     1.9 -
    1.10 -theory Spec
    1.11 -imports IOA Action
    1.12 -begin
    1.13 -
    1.14 -definition
    1.15 -  spec_sig :: "'m action signature" where
    1.16 -  sig_def: "spec_sig = (UN m.{S_msg(m)}, 
    1.17 -                        UN m.{R_msg(m)}, 
    1.18 -                        {})"
    1.19 -
    1.20 -definition
    1.21 -  spec_trans :: "('m action, 'm list)transition set" where
    1.22 -  trans_def: "spec_trans =
    1.23 -   {tr. let s = fst(tr);                            
    1.24 -            t = snd(snd(tr))                        
    1.25 -        in                                          
    1.26 -        case fst(snd(tr))                           
    1.27 -        of                                          
    1.28 -        S_msg(m) => t = s@[m]  |                    
    1.29 -        R_msg(m) => s = (m#t)  |                    
    1.30 -        S_pkt(pkt) => False |                    
    1.31 -        R_pkt(pkt) => False |                    
    1.32 -        S_ack(b) => False |                      
    1.33 -        R_ack(b) => False |                      
    1.34 -        C_m_s => False |                            
    1.35 -        C_m_r => False |                            
    1.36 -        C_r_s => False |                            
    1.37 -        C_r_r(m) => False}"
    1.38 -
    1.39 -definition
    1.40 -  spec_ioa :: "('m action, 'm list)ioa" where
    1.41 -  ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
    1.42 -
    1.43 -end