(* Title: HOL/IOA/NTP/Receiver.ML ID: $Id: Receiver.ML,v 1.7 2005/09/03 14:50:25 wenzelm Exp $ Author: Tobias Nipkow & Konrad Slind *) Goal "S_msg(m) ~: actions(receiver_asig) & \ \ R_msg(m) : actions(receiver_asig) & \ \ S_pkt(pkt) ~: actions(receiver_asig) & \ \ R_pkt(pkt) : actions(receiver_asig) & \ \ S_ack(b) : actions(receiver_asig) & \ \ R_ack(b) ~: actions(receiver_asig) & \ \ C_m_s ~: actions(receiver_asig) & \ \ C_m_r : actions(receiver_asig) & \ \ C_r_s ~: actions(receiver_asig) & \ \ C_r_r(m) : actions(receiver_asig)"; by (simp_tac (simpset() addsimps (receiver_asig_def :: actions_def :: asig_projections)) 1); qed "in_receiver_asig"; val receiver_projections = [rq_def, rsent_def, rrcvd_def, rbit_def, rsending_def];