--- a/IOA/example/Spec.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Spec.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* 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
@@ -6,13 +14,13 @@
spec_trans :: "('m action, 'm list)transition set"
spec_ioa :: "('m action, 'm list)ioa"
-rules
+defs
sig_def "spec_sig == <UN m.{S_msg(m)}, \
\ UN m.{R_msg(m)}, \
\ {}>"
-trans_def "spec_trans = \
+trans_def "spec_trans == \
\ {tr. let s = fst(tr); \
\ t = snd(snd(tr)) \
\ in \