Old_HOL: IOA/example/Action.thy@f04b33ce250f (annotated)

168 44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	1	(* Title: HOL/IOA/example/Action.thy
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	2	ID: $Id$
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	4	Copyright 1994 TU Muenchen
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	5
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	6	The set of all actions of the system
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	7	*)
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	8
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	9	Action = Packet +
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	10	datatype 'm action = S_msg ('m) \| R_msg ('m)
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	11	\| S_pkt ('m packet) \| R_pkt ('m packet)
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	12	\| S_ack (bool) \| R_ack (bool)
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	13	\| C_m_s \| C_m_r \| C_r_s \| C_r_r ('m)
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	14	end

author	clasohm
	Tue, 24 Oct 1995 14:59:17 +0100
changeset 251	f04b33ce250f
parent 168	44ff2275d44f
permissions	-rw-r--r--