diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Spec.thy
--- a/IOA/example/Spec.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      HOL/IOA/example/Spec.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
-
-The specification of reliable transmission
-*)
-
-Spec = List + IOA + Action +
-
-consts
-
-spec_sig   :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa   :: "('m action, 'm list)ioa"
-
-defs
-
-sig_def "spec_sig == <UN m.{S_msg(m)}, 
-                     UN m.{R_msg(m)}, 
-                     {}>"
-
-trans_def "spec_trans ==                           
- {tr. let s = fst(tr);                            
-          t = snd(snd(tr))                        
-      in                                          
-      case fst(snd(tr))                           
-      of                                          
-      S_msg(m) => t = s@[m]  |                    
-      R_msg(m) => s = (m#t)  |                    
-      S_pkt(pkt) => False |                    
-      R_pkt(pkt) => False |                    
-      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}"
-
-ioa_def "spec_ioa == <spec_sig, {[]}, spec_trans>"
-
-end