IOA/example/Action.thy
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