isabelle: src/HOLCF/IOA/NTP/Packet.ML@213dcc39358f (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	kleing
	Tue, 13 May 2003 08:59:21 +0200
changeset 14024	213dcc39358f
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--