diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Action.thy --- 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