diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Channels.thy
--- a/IOA/example/Channels.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  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
-
-srch_asig, 
-rsch_asig  :: "'m action signature"
-
-srch_trans :: "('m action, 'm packet multiset)transition set"
-rsch_trans :: "('m action, bool multiset)transition set"
-
-srch_ioa   :: "('m action, 'm packet multiset)ioa"
-rsch_ioa   :: "('m action, bool multiset)ioa"
-
-defs
-
-srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    
-                            UN pkt. {R_pkt(pkt)},    
-                            {}>"
-
-rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, 
-                            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 |                                     
-           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_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 |                            
-      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_r_r(m) => False}"
-
-
-srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
-rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>"
-
-end