Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IOA/NTP/Receiver.thy
changeset 67613 ce654b0e6d69
parent 66453 cc19f7ca2ed6 
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -79,16 +79,16 @@
     (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
 
 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)"
+  "S_msg(m) \<notin> actions(receiver_asig)"
+  "R_msg(m) \<in> actions(receiver_asig)"
+  "S_pkt(pkt) \<notin> actions(receiver_asig)"
+  "R_pkt(pkt) \<in> actions(receiver_asig)"
+  "S_ack(b) \<in> actions(receiver_asig)"
+  "R_ack(b) \<notin> actions(receiver_asig)"
+  "C_m_s \<notin> actions(receiver_asig)"
+  "C_m_r \<in> actions(receiver_asig)"
+  "C_r_s \<notin> actions(receiver_asig)"
+  "C_r_r(m) \<in> 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
isabelle