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

author	haftmann
	Tue, 20 Mar 2007 15:52:39 +0100
changeset 22482	8fc3d7237e03
parent 19738	1ac610922636
child 35174	e15040ae75d7
permissions	-rw-r--r--