src/HOLCF/IOA/NTP/Action.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
--- a/src/HOLCF/IOA/NTP/Action.thy	Sat Nov 27 14:34:54 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      HOL/IOA/NTP/Action.thy
-    Author:     Tobias Nipkow & Konrad Slind
-*)
-
-header {* The set of all actions of the system *}
-
-theory Action
-imports Packet
-begin
-
-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