isabelle: src/HOLCF/IOA/NTP/Receiver.ML@fc385ce6187d (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/Receiver.ML
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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	6	Goal
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	"S_msg(m) ~: actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	\ R_msg(m) : actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9	\ S_pkt(pkt) ~: actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	\ R_pkt(pkt) : actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	\ S_ack(b) : actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12	\ R_ack(b) ~: actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	\ C_m_s ~: actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	\ C_m_r : actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	\ C_r_s ~: actions(receiver_asig) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	\ C_r_r(m) : actions(receiver_asig)";
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	by (simp_tac (simpset() addsimps (receiver_asig_def :: actions_def ::
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	asig_projections)) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	qed "in_receiver_asig";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	val receiver_projections =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	[rq_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	rsent_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	rrcvd_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	rbit_def,
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	rsending_def];

author	aspinall
	Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740	fc385ce6187d
parent 17244	0b2ff9541727
permissions	-rw-r--r--