Some definitions of interest.
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
Msg_sub	Def Msg_sub(l; M) == {m:Msg(M)| haslink(l; m) }
	Thm* M:(IdLnkIdType), l:IdLnk. Msg_sub(l; M)  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
eventtype	Def eventtype(k;loc;V;M;e) == kindcase(k(e);a.V(loc(e),a);l,t.M(l,t))
	Thm* E:Type, V:(IdIdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), Thm* e:E. eventtype(k;loc;V;M;e)  Type
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
strongwellfounded	Def SWellFounded(R(x;y)) == f:(T). x,y:T. R(x;y)  f(x)<f(y)
	Thm* T:Type, R:(TTType). SWellFounded(R(x,y))  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
tagof	Def tag(k) == 2of(outl(k))
	Thm* k:Knd. isrcv(k)  tag(k)  Id
trans	Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)
	Thm* T:Type, E:(TTProp). (Trans x,y:T. E(x,y))  Prop

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