--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,27 @@
+(* Title: HOL/IOA/NTP/Packet.thy
+ Author: Tobias Nipkow & Konrad Slind
+*)
+
+theory Packet
+imports Multiset
+begin
+
+types
+ 'msg packet = "bool * 'msg"
+
+definition
+ hdr :: "'msg packet => bool" where
+ "hdr == fst"
+
+definition
+ msg :: "'msg packet => 'msg" where
+ "msg == snd"
+
+
+text {* Instantiation of a tautology? *}
+lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)"
+ by simp
+
+declare hdr_def [simp] msg_def [simp]
+
+end