src/HOL/HOLCF/IOA/ABP/Packet.thy
changeset 40774 0437dbc127b3
parent 35174 e15040ae75d7
child 40945 b8703f63bfb2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,22 @@
+(*  Title:      HOLCF/IOA/ABP/Packet.thy
+    Author:     Olaf Müller
+*)
+
+header {* Packets *}
+
+theory Packet
+imports Main
+begin
+
+types
+  'msg packet = "bool * 'msg"
+
+definition
+  hdr :: "'msg packet => bool" where
+  "hdr = fst"
+
+definition
+  msg :: "'msg packet => 'msg" where
+  "msg = snd"
+
+end