isabelle: src/HOL/HOLCF/IOA/ABP/Action.thy@6d736d983d5c (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/Action.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
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* The set of all actions of the system *}
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 Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	datatype 'm action =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	Next \| S_msg 'm \| R_msg 'm
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	\| S_pkt "'m packet" \| R_pkt "'m packet"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	\| S_ack bool \| R_ack bool
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	end

author	wenzelm
	Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648	6d736d983d5c
parent 40945	b8703f63bfb2
child 42151	4da4fc77664b
permissions	-rw-r--r--