isabelle: src/HOL/IOA/NTP/Receiver.ML@0140ff702b23 (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Receiver.ML
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
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	goal Receiver.thy
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8	"S_msg(m) ~: actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	9	\ R_msg(m) : actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10	\ S_pkt(pkt) ~: actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	11	\ R_pkt(pkt) : actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12	\ S_ack(b) : actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	13	\ R_ack(b) ~: actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	14	\ C_m_s ~: actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	15	\ C_m_r : actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	16	\ C_r_s ~: actions(receiver_asig) & \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	17	\ C_r_r(m) : actions(receiver_asig)";
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	18	by(simp_tac (action_ss addsimps
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	19	(Receiver.receiver_asig_def :: actions_def ::
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	20	asig_projections @ set_lemmas)) 1);
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	21	qed "in_receiver_asig";
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	22
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	23	val receiver_projections =
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	24	[Receiver.rq_def,
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	25	Receiver.rsent_def,
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	26	Receiver.rrcvd_def,
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	27	Receiver.rbit_def,
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	28	Receiver.rsending_def];
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	29
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	30

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 1051	4fcd0638e61d
child 1266	3ae9fe3c0f68
permissions	-rw-r--r--