src/HOL/IOA/ABP/Action.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1138 82fd99d5a6ff
permissions -rw-r--r--
Dep. on Provers/nat_transitive
mueller@1138
     1
(*  Title:      HOL/IOA/example/Action.thy
nipkow@1050
     2
    ID:         $Id$
mueller@1138
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1138
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
The set of all actions of the system
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Action = Packet +
nipkow@1050
    10
datatype 'm action = Next | S_msg ('m) | R_msg ('m)
nipkow@1050
    11
                   | S_pkt ('m packet) | R_pkt ('m packet) 
nipkow@1050
    12
                   | S_ack (bool) | R_ack (bool)         
nipkow@1050
    13
end