--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Packet.thy	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,18 @@
+Packet = Arith +
+
+types
+
+   'msg packet = "bool * 'msg"
+
+consts
+
+  hdr  :: "'msg packet => bool"
+  msg :: "'msg packet => 'msg"
+
+rules
+
+  hdr_def "hdr == fst"
+
+  msg_def "msg == snd"
+
+end