isabelle: src/HOLCF/IOA/NTP/Packet.thy@f88a91ff8ac6 (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
12218 6597093b77e7 GPLed; wenzelm parents: 10212 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: 10212 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
10212 33fe2d701ddd * empty log message * nipkow parents: 3073 diff changeset	9	Packet = Multiset +
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	types
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	'msg packet = "bool * 'msg"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	constdefs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	hdr :: 'msg packet => bool
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	"hdr == fst"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	msg :: 'msg packet => 'msg
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21	"msg == snd"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	end

author	berghofe
	Mon, 05 Aug 2002 14:35:33 +0200
changeset 13455	f88a91ff8ac6
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--