Def		x,y,z. t(x;y;z)	[so_lambda3]
Def		...	[hide]
Def		Decision	[decision]
Def		dec2bool(d)	[dec2bool]
Def		increasing(f;k)	[increasing]
Def		A & B	[cand]	core
Def		P  Q	[iff]	core
Def		P  Q	[implies]	core
Def		Prop	[prop]	core
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		Dec(P)	[decidable]	core
Def		Top	[top]	core
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		{i..j}	[int_seg]	int 1
Def		x:A. B(x)	[all]	core
Def		P  Q	[rev_implies]	core
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		hd(l)	[hd]	list 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		tl(l)	[tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		b	[bnot]	bool 1

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