src/HOLCF/IOA/NTP/Packet.thy

--- a/src/HOLCF/IOA/NTP/Packet.thy	Sat May 27 19:49:36 2006 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.thy	Sat May 27 21:00:31 2006 +0200
@@ -18,6 +18,11 @@
   msg :: "'msg packet => 'msg"
   "msg == snd"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+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