isabelle: src/HOLCF/IOA/NTP/Action.thy@0b2ff9541727 (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Action.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
88366253a09a Old NTP 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 = 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	\| C_m_s \| C_m_r \| C_r_s \| C_r_r 'm
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	16
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	end

author	wenzelm
	Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244	0b2ff9541727
parent 14981	e73f8140af78
child 19739	c58ef2aa5430
permissions	-rw-r--r--