src/HOLCF/IOA/NTP/Packet.ML

--- a/src/HOLCF/IOA/NTP/Packet.ML	Sat May 27 19:49:36 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      HOL/IOA/NTP/Packet.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-
-Packets.
-*)
-
-(* Instantiation of a tautology? *)
-Goal "!x. x = packet --> hdr(x) = hdr(packet)";
- by (simp_tac (simpset() addsimps [hdr_def]) 1);
-qed "eq_packet_imp_eq_hdr"; 
-
-Addsimps [hdr_def,msg_def];