isabelle: src/HOLCF/IOA/NTP/Packet.thy@4efb68e5576d (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.thy
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	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	theory Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	imports Multiset
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	types
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	'msg packet = "bool * 'msg"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	constdefs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	hdr :: "'msg packet => bool"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	"hdr == fst"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	msg :: "'msg packet => 'msg"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	"msg == snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	21
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	22	text {* Instantiation of a tautology? *}
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	23	lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	24	by simp
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	25
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	26	declare hdr_def [simp] msg_def [simp]
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	27
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	end

author	wenzelm
	Mon, 08 Oct 2007 18:13:10 +0200
changeset 24911	4efb68e5576d
parent 19739	c58ef2aa5430
child 25131	2c8caac48ade
permissions	-rw-r--r--