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