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, x,i:Id, T:Type, c:T. Thm* (x,y:T. Dec(x = y  T)) Thm*  Thm* (vartype(i;x) r T) Thm*  Thm* (e:E. loc(e) = i  Id  first(e)  (x when e) = c  T) Thm*  Thm* (e':E.  Thm* (loc(e') = i  Id Thm* ( Thm* ((x after e') = c  T Thm* ( Thm* ((ev:E. ev  e'  & (x after ev) = (x when ev)  T))	[change-since-init]
Thm* es:ES, x,i:Id, T:Type. Thm* (x,y:T. Dec(x = y  T)) Thm*  Thm* (vartype(i;x) r T) Thm*  Thm* (e',e:E. Thm* (e  e'  Thm* ( Thm* (loc(e') = i  Id Thm* ( Thm* ((x after e') = (x when e)  T Thm* ( Thm* ((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T))	[change-lemma]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). e@i.P(e)  Prop	[existse-at_wf]
Thm* es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop). Thm* e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)	[alle-at-iff]
Thm* es:ES, x:Id, e:E. Thm* first(e)  (x after pred(e)) = (x when e)  vartype(loc(e);x)	[es-after-pred]
Thm* es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List	[es-interval_wf2]
Def e@i.P(e) == e:E. loc(e) = i  Id & P(e)	[existse-at]
Def e@i.P(e) == e:E. loc(e) = i  Id  P(e)	[alle-at]

In prior sections: mb event system 2

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