diff -r 1ac610922636 -r c58ef2aa5430 src/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOLCF/IOA/NTP/Receiver.thy	Sat May 27 19:49:36 2006 +0200
+++ b/src/HOLCF/IOA/NTP/Receiver.thy	Sat May 27 21:00:31 2006 +0200
@@ -87,6 +87,19 @@
 receiver_ioa_def: "receiver_ioa ==
  (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma in_receiver_asig:
+  "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_all add: receiver_asig_def actions_def asig_projections)
+
+lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def
 
 end