src/HOLCF/IOA/ABP/Packet.thy
changeset 19738 1ac610922636
parent 17244 0b2ff9541727
child 25131 2c8caac48ade
equal deleted inserted replaced
19737:3b8920131be2 19738:1ac610922636
    17   "hdr == fst"
    17   "hdr == fst"
    18 
    18 
    19   msg :: "'msg packet => 'msg"
    19   msg :: "'msg packet => 'msg"
    20   "msg == snd"
    20   "msg == snd"
    21 
    21 
    22 ML {* use_legacy_bindings (the_context ()) *}
       
    23 
       
    24 end
    22 end