author | mueller |
Mon, 13 Nov 1995 12:06:57 +0100 | |
changeset 1328 | 9a449a91425d |
parent 1266 | 3ae9fe3c0f68 |
permissions | -rw-r--r-- |
(* 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];