src/HOLCF/IOA/NTP/Receiver.ML
changeset 5068 fb28eaa07e01
parent 4423 a129b817b58a
child 12218 6597093b77e7
equal deleted inserted replaced
5067:62b6288e6005 5068:fb28eaa07e01
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     4     Copyright   1994  TU Muenchen
     5 *)
     5 *)
     6 
     6 
     7 goal Receiver.thy
     7 Goal
     8  "S_msg(m) ~: actions(receiver_asig)      &   \
     8  "S_msg(m) ~: actions(receiver_asig)      &   \
     9 \ R_msg(m) : actions(receiver_asig)       &   \
     9 \ R_msg(m) : actions(receiver_asig)       &   \
    10 \ S_pkt(pkt) ~: actions(receiver_asig) &   \
    10 \ S_pkt(pkt) ~: actions(receiver_asig) &   \
    11 \ R_pkt(pkt) : actions(receiver_asig)  &   \
    11 \ R_pkt(pkt) : actions(receiver_asig)  &   \
    12 \ S_ack(b) : actions(receiver_asig)    &   \
    12 \ S_ack(b) : actions(receiver_asig)    &   \