isabelle: src/HOLCF/IOA/ABP/Packet.thy@6f79698f294d (annotated)

3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Packet.thy
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 10215 diff changeset	3	Author: Olaf M�ller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
a31419014be5 Old ABP 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	header {* Packets *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Main
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	types
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	'msg packet = "bool * 'msg"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	15	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	16	hdr :: "'msg packet => bool" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	17	"hdr = fst"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	19	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	20	msg :: "'msg packet => 'msg" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19738 diff changeset	21	"msg = snd"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	end

author	wenzelm
	Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456	6f79698f294d
parent 25131	2c8caac48ade
child 35174	e15040ae75d7
permissions	-rw-r--r--