diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/IOA.thy
--- a/IOA/meta_theory/IOA.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/IOA.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,10 @@
-(* The I/O automata of Lynch and Tuttle. *)
+(*  Title:      HOL/IOA/meta_theory/IOA.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The I/O automata of Lynch and Tuttle.
+*)
 
 IOA = Asig +
 
@@ -51,7 +57,7 @@
   ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
 
 
-rules
+defs
 
 state_trans_def
   "state_trans(asig,R) == \
@@ -59,9 +65,9 @@
   \  (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
 
 
-ioa_projections_def
-   "asig_of = fst  &  starts_of = (fst o snd)  &  trans_of = (snd o snd)"
-
+asig_of_def   "asig_of == fst"
+starts_of_def "starts_of == (fst o snd)"
+trans_of_def  "trans_of == (snd o snd)"
 
 ioa_def
   "IOA(ioa) == (is_asig(asig_of(ioa))      &                            \