Def		implies	[himplies]	hol min
Def		res_forall	[hres_forall]
Def		equal	[hequal]	hol min
Def		hbool	[hbool]	hol min
Def		'a  'b	[hfun]	hol min
Def		all	[hall]	hol bool
Def		S	[stype]	hol
Def		and	[hand]	hol bool
Def		exists	[hexists]	hol bool
Def		res_exists	[hres_exists]
Def		select	[hselect]	hol min
Def		res_select	[hres_select]
Def		t	[ht]	hol bool
Def		arb	[harb]
Def		cond	[hcond]	hol bool
Def		res_abstract	[hres_abstract]
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		res_choose('a;x.P(x);x.Q(x))	[res_choose]
Def		@x:'a. p(x)	[bchoose]	hol min
Def		@x:T. P(x)	[choose]	hol
Def		res_lambda('a;'b;x.P(x);x.f(x))	[res_lambda]
Def		arb(T)	[arb]	hol
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		x:T. b(x)	[tlambda]	fun 1
Def		x:T. P(x)	[ball]	hol
Def		x:T. P(x)	[bexists]	hol
Def		b	[assert]	bool 1
Def		res_all('a;x.P(x);x.Q(x))	[res_all]
Def		x = y	[bequal]	hol
Def		P	[prop_to_bool]	hol
Def			[bool]	bool 1
Def		res_exists('a;x.P(x);x.Q(x))	[res_exists]
Def		pq	[bimplies]	bool 1
Def		pq	[band]	bool 1
Def		b	[bnot]	bool 1
Def		p  q	[bor]	bool 1

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