Def (e <loc e') == loc(e) = loc(e')  Id & (e < e')

is mentioned by

Thm* the_es:ES, e',e:E. (e  before(e'))  (e <loc e')

[member-es-before]

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