--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Channels.ML Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,39 @@
+local
+val SS = action_ss addsimps
+ (Channels.srch_asig_def ::
+ Channels.rsch_asig_def ::
+ actions_def :: asig_projections_def :: set_lemmas)
+in
+val _ = goal Channels.thy
+ "S_msg(m) ~: actions(srch_asig) & \
+ \ R_msg(m) ~: actions(srch_asig) & \
+ \ S_pkt(pkt) : actions(srch_asig) & \
+ \ R_pkt(pkt) : actions(srch_asig) & \
+ \ S_ack(b) ~: actions(srch_asig) & \
+ \ R_ack(b) ~: actions(srch_asig) & \
+ \ C_m_s ~: actions(srch_asig) & \
+ \ C_m_r ~: actions(srch_asig) & \
+ \ C_r_s ~: actions(srch_asig) & \
+ \ C_r_r(m) ~: actions(srch_asig)";
+
+val _ = by (simp_tac SS 1);
+
+val in_srch_asig = result();
+
+val _ = goal Channels.thy
+ "S_msg(m) ~: actions(rsch_asig) & \
+ \ R_msg(m) ~: actions(rsch_asig) & \
+ \ S_pkt(pkt) ~: actions(rsch_asig) & \
+ \ R_pkt(pkt) ~: actions(rsch_asig) & \
+ \ S_ack(b) : actions(rsch_asig) & \
+ \ R_ack(b) : actions(rsch_asig) & \
+ \ C_m_s ~: actions(rsch_asig) & \
+ \ C_m_r ~: actions(rsch_asig) & \
+ \ C_r_s ~: actions(rsch_asig) & \
+ \ C_r_r(m) ~: actions(rsch_asig)";
+
+val _ = by (simp_tac SS 1);
+
+val in_rsch_asig = result();
+
+end;