src/HOL/IOA/NTP/Packet.ML
author paulson
Mon, 07 Oct 1996 10:28:44 +0200
changeset 2056 93c093620c28
parent 1328 9a449a91425d
permissions -rw-r--r--
Removed commands made redundant by new one-point rules

(*  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];