diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Spec.thy
--- 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                                          \