src/HOLCF/IOA/ABP/Action.thy
author wenzelm
Sat Sep 03 16:50:22 2005 +0200 (2005-09-03)
changeset 17244 0b2ff9541727
parent 14981 e73f8140af78
child 19738 1ac610922636
permissions -rw-r--r--
converted to Isar theory format;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Action.thy
mueller@3072
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3072
     4
*)
mueller@3072
     5
wenzelm@17244
     6
header {* The set of all actions of the system *}
wenzelm@17244
     7
wenzelm@17244
     8
theory Action
wenzelm@17244
     9
imports Packet
wenzelm@17244
    10
begin
wenzelm@17244
    11
wenzelm@17244
    12
datatype 'm action =
wenzelm@17244
    13
    Next | S_msg 'm | R_msg 'm
wenzelm@17244
    14
  | S_pkt "'m packet" | R_pkt "'m packet"
wenzelm@17244
    15
  | S_ack bool | R_ack bool
wenzelm@17244
    16
wenzelm@17244
    17
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17244
    18
mueller@3072
    19
end