mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def 1of(t) == t.1

is mentioned by

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: core mb list 1 mb event system 1 mb event system 2 mb event system 3 mb event system 4

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

mb event system 5 Sections EventSystems Doc