| author | wenzelm |
| Tue, 27 May 1997 15:45:07 +0200 | |
| changeset 3362 | 0b268cff9344 |
| parent 3073 | 88366253a09a |
| child 4098 | 71e05eb27fb6 |
| 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];