Def		SQType(T)	[sq_type]
Def			[nat]	int 1
Def			[bool]	bool 1
Def		true	[btrue]	bool 1
Def		false	[bfalse]	bool 1
Def		i=j	[eq_int]	bool 1
Def		a  b	[nequal]	core
Def		AB	[le]	core
Def		A	[not]	core
Def		i<j	[lt_int]	bool 1
Def		x=yAtom	[eq_atom]	bool 1
Def		P  Q	[or]	core
Def		{T}	[guard]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core

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