Def		o	[ho]
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		x:T. P(x)	[ball]	hol
Def		b	[assert]	bool 1
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def		k	[hk]
Def		s	[hs]
Def		i	[hi]
Def		and	[hand]	hol bool
Def		P & Q	[and]	core
Def		f o g	[compose]	fun 1
Def		x:T. b(x)	[tlambda]	fun 1
Def		'a  'b	[hfun]	hol min
Def		x = y	[bequal]	hol
Def		pq	[band]	bool 1
Def		P	[prop_to_bool]	hol

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