Some definitions of interest.
msga	Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
	Thm* MsgA  Type{i'}
ma-state	Def State(ds) == x:Idds(x)?Top
ma-valtype	Def ma-valtype(da; k) == da(k)?Top
Id	Def Id == Atom
	Thm* Id  Type
fpf	Def a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
	Thm* A:Type, B:(AType). a:A fp-> B(a)  Type
ma-single-pre	Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )
fpf-single	Def x : v == <[x],x.v>
locl	Def locl(a) == inr(a)
	Thm* a:Id. locl(a)  Knd
so_lambda1	Def (1. b(1))(1) == b(1)

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