src/HOL/IOA/NTP/Packet.ML
changeset 1051 4fcd0638e61d
child 1266 3ae9fe3c0f68
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/NTP/Packet.ML	Thu Apr 13 16:57:18 1995 +0200
@@ -0,0 +1,13 @@
+(*  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 (HOL_ss addsimps [Packet.hdr_def]) 1);
+qed "eq_packet_imp_eq_hdr"; 
\ No newline at end of file