--- 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