src/HOLCF/IOA/NTP/Packet.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/NTP/Packet.ML	Wed Apr 30 11:25:31 1997 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/IOA/NTP/Packet.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+Packets
+*)
+
+
+(* Instantiation of a tautology? *)
+goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
+ by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1);
+qed "eq_packet_imp_eq_hdr"; 
+
+Addsimps [Packet.hdr_def,Packet.msg_def];