Def Knd == (IdLnkId)+Id

is mentioned by

Thm* the_w:World, i:Id, k:Knd. V(i;k)  Type	[w-V_wf]
Thm* the_w:World, e:E. kind(e)  Knd	[w-ekind_wf]
Thm* the_w:World, i:Id, a:Action(i). isnull(a)  kind(a)  Knd	[w-kind_wf]
Thm* i:Id, TA:(IdIdType), M:(IdLnkIdType). Thm* w-action-dec(TA;M;i)  KndType	[w-action-dec_wf]
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]
Def action(dec) == Unit+(k:Knddec(k))	[action]

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