Some definitions of interest.
Dconstant	Def Dconstant(loc;T;c;x;i) Def == if loc = i [x : T initially x = c; only members of nil affect x :T] Def == else nil fi
	Thm* loc:Id, T:Type, c:T, x,i:Id. Dconstant(loc;T;c;x;i)  MsgA List
d-feasible	Def d-feasible(D) Def == (i:Id. Feasible(M(i))) Def == & (l:IdLnk, tg:Id. Def == & (M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)) Def == & (i:Id.  Def == & (finite-type({l:IdLnk Def == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))
ma-join-list	Def (L) == reduce(A,B. A  B;;L)
Id	Def Id == Atom
	Thm* Id  Type

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