Some definitions of interest.
event_system	Def ES Def == E:Type Def == EqDecider(E)(T:IdIdType Def == EqDecider(E)(V:IdIdType Def == EqDecider(E)(M:IdLnkIdType Def == EqDecider(E)(Top(loc:EId Def == EqDecider(E)(Top(kind:EKnd Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e)) Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List)) Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e)) Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||) Def == EqDecider(E)(Top(first:E Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E Def == EqDecider(E)(Top(causl:EEProp Def == EqDecider(E)(Top(ESAxioms{i:l} Def == EqDecider(E)(Top(ESAxioms(E; Def == EqDecider(E)(Top(ESAxioms(T; Def == EqDecider(E)(Top(ESAxioms(M; Def == EqDecider(E)(Top(ESAxioms(loc; Def == EqDecider(E)(Top(ESAxioms(kind; Def == EqDecider(E)(Top(ESAxioms(val; Def == EqDecider(E)(Top(ESAxioms(when; Def == EqDecider(E)(Top(ESAxioms(after; Def == EqDecider(E)(Top(ESAxioms(sends; Def == EqDecider(E)(Top(ESAxioms(sender; Def == EqDecider(E)(Top(ESAxioms(index; Def == EqDecider(E)(Top(ESAxioms(first; Def == EqDecider(E)(Top(ESAxioms(pred; Def == EqDecider(E)(Top(ESAxioms(causl) Def == EqDecider(E)(Top(Top))
	Thm* ES  Type{i'}
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
es-E	Def E == 1of(es)
es-kind	Def kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e)
es-loc	Def loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e)
es-sender	Def sender(e) Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))))(e)
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
tagof	Def tag(k) == 2of(outl(k))
	Thm* k:Knd. isrcv(k)  tag(k)  Id
outl	Def outl(x) == InjCase(x; y. y; z. "???")
	Thm* A,B:Type, x:A+B. isl(x)  outl(x)  A
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
rcv	Def rcv(l; tg) == inl(<l,tg>)
	Thm* l:IdLnk, tg:Id. rcv(l; tg)  Knd

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html