Def		hbool	[hbool]
Def		hind	[hind]
Def		'a  'b	[hfun]
Def		equal	[hequal]
Def		implies	[himplies]
Def		select	[hselect]
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def		@x:'a. p(x)	[bchoose]
Def		b	[assert]	bool 1
Def		@x:T. P(x)	[choose]	hol
Def			[bool]	bool 1
Def			[nat]	int 1
Def		x = y	[bequal]	hol
Def		x:T. b(x)	[tlambda]	fun 1
Def		pq	[bimplies]	bool 1
Def		arb(T)	[arb]	hol
Def		AB	[le]	core
Def		P	[prop_to_bool]	hol
Def		b	[bnot]	bool 1
Def		p  q	[bor]	bool 1
Def		A	[not]	core

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