isabelle: src/HOL/IOA/NTP/Packet.ML@b50b8c0eec01 (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)";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1051 diff changeset	12	by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1);
1328 9a449a91425d * empty log message * mueller parents: 1266 diff changeset	13	qed "eq_packet_imp_eq_hdr";
9a449a91425d * empty log message * mueller parents: 1266 diff changeset	14
9a449a91425d * empty log message * mueller parents: 1266 diff changeset	15	Addsimps [Packet.hdr_def,Packet.msg_def];

author	paulson
	Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469	b50b8c0eec01
parent 1328	9a449a91425d
permissions	-rw-r--r--