is mentioned by

Thm* the_w:World.  Thm* FairFifo Thm*  Thm* ESAxioms{i:l} Thm* ESAxioms(E; Thm* ESAxioms((i,x. vartype(i;x)); Thm* ESAxioms(the_w.M; Thm* ESAxioms((e.loc(e)); Thm* ESAxioms((e.kind(e)); Thm* ESAxioms((e.val(e)); Thm* ESAxioms((x,e. (x when e)); Thm* ESAxioms((x,e. (x after e)); Thm* ESAxioms((l,e. sends(l;e)); Thm* ESAxioms((e.sender(e)); Thm* ESAxioms((e.index(e)); Thm* ESAxioms((e.first(e)); Thm* ESAxioms((e.pred(e)); Thm* ESAxioms((e,e'. e <c e'))	[world-event-system]
Thm* the_w:World, e,e':E. Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')	[w-locl-iff]
Thm* the_w:World, e:E, t:. Thm* FairFifo Thm*  Thm* isrcv(kind(e)) Thm*  Thm* match(lnk(kind(e));t;time(e)) Thm*  Thm* onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))|| Thm* -||snds(lnk(kind(e));t)||)] Thm* = Thm* msg(a(loc(e);time(e))) Thm*  Msg	[w-match-property]
Thm* the_w:World, e:E. Thm* FairFifo Thm*  Thm* isrcv(kind(e)) Thm*  Thm* (t:time(e).  Thm* (match(lnk(kind(e));t;time(e)) Thm* (& onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))|| Thm* (& -||snds(lnk(kind(e));t)||)] Thm* (& = Thm* (& msg(a(loc(e);time(e))) Thm* (&  Msg)	[better-w-match-exists]
Thm* the_w:World, e:E. <loc(e),time(e)> ~ e	[w-loc-time]
Thm* the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))	[assert-w-first]
Thm* the_w:World, x:Id, e:E. (x after e)  vartype(loc(e);x)	[w-after_wf]
Thm* the_w:World, x:Id, e:E. (x when e)  vartype(loc(e);x)	[w-when_wf]
Thm* the_w:World, e:E. val(e)  V(loc(e);kind(e))	[w-eval_wf]
Thm* the_w:World, e:E. act(e)  {a:Action(loc(e))| isnull(a) }	[w-act_wf]
Def ES(the_w;p) Def == <E Def == ,product-deq(Id;;IdDeq;NatDeq) Def == ,(i,x. vartype(i;x)) Def == ,(i,a. V(i;locl(a))) Def == ,the_w.M Def == , Def == ,(e.loc(e)) Def == ,(e.kind(e)) Def == ,(e.val(e)) Def == ,(x,e. (x when e)) Def == ,(x,e. (x after e)) Def == ,(l,e. sends(l;e)) Def == ,(e.sender(e)) Def == ,(e.index(e)) Def == ,(e.first(e)) Def == ,(e.pred(e)) Def == ,(e,e'. e <c e') Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p) Def == ,>	[w-es]
Def sends(l;e) == onlnk(l;m(loc(e);time(e)))	[w-sends]
Def e <loc e' == loc(e) = loc(e')  Id & time(e)<time(e')	[w-locl]
Def pred(e) Def == if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>) Def == else <loc(e),time(e)-1> fi Def (recursive)	[w-pred]
Def first(e) Def == if time(e)=0 true Def == i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>) Def == else false fi Def (recursive)	[w-first]

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