--- a/IOA/example/Action.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Action.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOL/IOA/example/Action.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The set of all actions of the system
+*)
+
 Action = Packet +
 datatype 'm action = S_msg ('m) | R_msg ('m)
                    | S_pkt ('m packet) | R_pkt ('m packet)