isabelle: src/HOL/IOA/NTP/Packet.ML@0140ff702b23 (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Packet.ML
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	2	ID: $Id$
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	5
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	6	Packets
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	*)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	9
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10	(* Instantiation of a tautology? *)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	11	goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12	by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1);
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	13	qed "eq_packet_imp_eq_hdr";