isabelle: src/HOLCF/IOA/NTP/Packet.ML@73de0ef7cb25 (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
12218 6597093b77e7 GPLed; wenzelm parents: 5068 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 5068 diff changeset	6	Packets.
3073 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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9	(* Instantiation of a tautology? *)
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4098 diff changeset	10	Goal "!x. x = packet --> hdr(x) = hdr(packet)";
4098 71e05eb27fb6 isatool fixclasimp; wenzelm parents: 3073 diff changeset	11	by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	qed "eq_packet_imp_eq_hdr";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	Addsimps [Packet.hdr_def,Packet.msg_def];

author	nipkow
	Fri, 15 Nov 2002 18:02:25 +0100
changeset 13716	73de0ef7cb25
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--