isabelle: src/HOLCF/IOA/NTP/Packet.ML@2b30ade8b35d (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Packet.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 5068 diff changeset	5	Packets.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	(* Instantiation of a tautology? *)
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4098 diff changeset	9	Goal "!x. x = packet --> hdr(x) = hdr(packet)";
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	by (simp_tac (simpset() addsimps [hdr_def]) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	qed "eq_packet_imp_eq_hdr";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	Addsimps [hdr_def,msg_def];

author	wenzelm
	Tue, 13 Sep 2005 22:19:32 +0200
changeset 17348	2b30ade8b35d
parent 17244	0b2ff9541727
permissions	-rw-r--r--