isabelle: src/HOL/IOA/ABP/Action.thy@0140ff702b23 (annotated)

1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	1	(* Title: HOL/IOA/ABP/Action.thy
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	3	Author: Tobias Nipkow & Olaf Mueller
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	5
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	6	The set of all actions of the system
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	7	*)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	8
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	9	Action = Packet +
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	10	datatype 'm action = Next \| S_msg ('m) \| R_msg ('m)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	11	\| S_pkt ('m packet) \| R_pkt ('m packet)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	12	\| S_ack (bool) \| R_ack (bool)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	13	end