mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def rcv(l; tg) == inl(<l,tg>)

is mentioned by

Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg)
Thm* 
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)		[es-kind-rcv]
Thm* es:ES, l:IdLnk, tg:Id, e:E.
Thm* isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l; tg)		[es-rcv-kind]

In prior sections: mb event system 1 mb event system 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 3 Sections EventSystems Doc