Def da-outlinks(da;i)
Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg  da-outlinks(da1  da2;i)) Thm*  Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))	[da-outlinks-join]
Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg  da-outlinks(k : T;i)) Thm*  Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]

In prior sections: mb event system 4

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