changeset 252 | a4dc62a46ee4 |
parent 251 | f04b33ce250f |
child 253 | 132634d24019 |
--- a/IOA/example/Action.thy Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* 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) - | S_ack (bool) | R_ack (bool) - | C_m_s | C_m_r | C_r_s | C_r_r ('m) -end