src/HOLCF/IOA/ABP/Action.thy
changeset 17244 0b2ff9541727
parent 14981 e73f8140af78
child 19738 1ac610922636
--- a/src/HOLCF/IOA/ABP/Action.thy	Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/ABP/Action.thy	Sat Sep 03 16:50:22 2005 +0200
@@ -1,12 +1,19 @@
 (*  Title:      HOLCF/IOA/ABP/Action.thy
     ID:         $Id$
     Author:     Olaf Müller
-
-The set of all actions of the system.
 *)
 
-Action = Packet + Datatype +
-datatype 'm action = Next | S_msg ('m) | R_msg ('m)
-                   | S_pkt ('m packet) | R_pkt ('m packet) 
-                   | S_ack (bool) | R_ack (bool)         
+header {* The set of all actions of the system *}
+
+theory Action
+imports Packet
+begin
+
+datatype 'm action =
+    Next | S_msg 'm | R_msg 'm
+  | S_pkt "'m packet" | R_pkt "'m packet"
+  | S_ack bool | R_ack bool
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end