isabelle: src/HOL/IOA/NTP/Action.thy@840554ac0451 (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Action.thy
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	2	ID: $Id$
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	5
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	6	The set of all actions of the system
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	*)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	9	Action = Packet +
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10	datatype 'm action = S_msg ('m) \| R_msg ('m)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	11	\| S_pkt ('m packet) \| R_pkt ('m packet)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12	\| S_ack (bool) \| R_ack (bool)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	13	\| C_m_s \| C_m_r \| C_r_s \| C_r_r ('m)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	14	end