isabelle: src/HOL/HOLCF/IOA/ABP/Packet.thy@0baae4311a9f (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IOA/ABP/Packet.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 diff changeset	2	Author: Olaf Müller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
58880 0baae4311a9f modernized header; wenzelm parents: 42151 diff changeset	5	section {* Packets *}
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Main
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
41476 0fa9629aa399 types -> type_synonym huffman parents: 40945 diff changeset	11	type_synonym
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	'msg packet = "bool * 'msg"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	14	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	15	hdr :: "'msg packet => bool" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	16	"hdr = fst"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	18	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	19	msg :: "'msg packet => 'msg" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	20	"msg = snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	end

author	wenzelm
	Sun, 02 Nov 2014 17:16:01 +0100
changeset 58880	0baae4311a9f
parent 42151	4da4fc77664b
child 62002	f1599e98c4d0
permissions	-rw-r--r--