isabelle: src/HOL/IOA/NTP/Packet.thy@23ceb1dc9755 (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Packet.thy
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	2	ID: $Id$
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	5
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	6	Packets
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	*)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8
1328 9a449a91425d * empty log message * mueller parents: 1051 diff changeset	9	Packet = Arith + Multiset +
1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	11	types
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	13	'msg packet = "bool * 'msg"
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	14
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	15	consts
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	16
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1328 diff changeset	17	hdr :: 'msg packet => bool
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1328 diff changeset	18	msg :: 'msg packet => 'msg
1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	19
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	20	defs
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	21
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	22	hdr_def "hdr == fst"
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	23	msg_def "msg == snd"
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	24
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	25	end

author	paulson
	Thu, 18 Jan 1996 10:38:29 +0100
changeset 1444	23ceb1dc9755
parent 1376	92f83b9d17e1
child 1570	fd1b9c721ac7
permissions	-rw-r--r--