src/HOL/HOLCF/IOA/NTP/Abschannel.thy
changeset 67613 ce654b0e6d69
parent 66453 cc19f7ca2ed6
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -102,28 +102,28 @@
   trans_of_def asig_projections
 
 lemma in_srch_asig: 
-     "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)"
+     "S_msg(m) \<notin> actions(srch_asig)        \<and>
+       R_msg(m) \<notin> actions(srch_asig)        \<and>
+       S_pkt(pkt) \<in> actions(srch_asig)    \<and>
+       R_pkt(pkt) \<in> actions(srch_asig)    \<and>     
+       S_ack(b) \<notin> actions(srch_asig)     \<and>     
+       R_ack(b) \<notin> actions(srch_asig)     \<and>     
+       C_m_s \<notin> actions(srch_asig)           \<and>     
+       C_m_r \<notin> actions(srch_asig)           \<and>     
+       C_r_s \<notin> actions(srch_asig)  & C_r_r(m) \<notin> actions(srch_asig)"
   by (simp add: unfold_renaming)
 
 lemma in_rsch_asig: 
-      "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)"
+      "S_msg(m) \<notin> actions(rsch_asig)         \<and>
+       R_msg(m) \<notin> actions(rsch_asig)         \<and>
+       S_pkt(pkt) \<notin> actions(rsch_asig)    \<and>
+       R_pkt(pkt) \<notin> actions(rsch_asig)    \<and>
+       S_ack(b) \<in> actions(rsch_asig)       \<and>
+       R_ack(b) \<in> actions(rsch_asig)       \<and>
+       C_m_s \<notin> actions(rsch_asig)            \<and>
+       C_m_r \<notin> actions(rsch_asig)            \<and>
+       C_r_s \<notin> actions(rsch_asig)            \<and>
+       C_r_r(m) \<notin> actions(rsch_asig)"
   by (simp add: unfold_renaming)
 
 lemma srch_ioa_thm: "srch_ioa =