isabelle: src/HOL/HOLCF/IOA/NTP/Action.thy@180f1b3508ed (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Action.thy
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* The set of all actions of the system *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Packet
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10
58249 180f1b3508ed use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries blanchet parents: 42151 diff changeset	11	datatype_new 'm action = S_msg 'm \| R_msg 'm
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	\| S_pkt "'m packet" \| R_pkt "'m packet"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13	\| S_ack bool \| R_ack bool
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	\| C_m_s \| C_m_r \| C_r_s \| C_r_r 'm
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	end

author	blanchet
	Tue, 09 Sep 2014 20:51:36 +0200
changeset 58249	180f1b3508ed
parent 42151	4da4fc77664b
child 58310	91ea607a34d8
permissions	-rw-r--r--