diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Asig.thy
--- a/IOA/meta_theory/Asig.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Asig.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOL/IOA/meta_theory/Asig.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+Action signatures
+*)
+
 Asig = Option +
 
 types 
@@ -11,10 +19,11 @@
   mk_ext_asig   ::"'action signature => 'action signature"
 
 
-rules
+defs
 
-asig_projections_def
-   "inputs = fst  & outputs = (fst o snd)  & internals = (snd o snd)"
+asig_inputs_def    "inputs == fst"
+asig_outputs_def   "outputs == (fst o snd)"
+asig_internals_def "internals == (snd o snd)"
 
 actions_def
    "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"