Def		curry	[hcurry]
Def		hprod('a; 'b)	[hprod]
Def		'a  'b	[hfun]	hol min
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def		and	[hand]	hol bool
Def		hbool	[hbool]	hol min
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		exists	[hexists]	hol bool
Def		is_pair	[his_pair]
Def		select	[hselect]	hol min
Def		type_definition	[htype_definition]	hol bool
Def		x:T. P(x)	[bexists]	hol
Def		x:T. P(x)	[ball]	hol
Def		@x:'a. p(x)	[bchoose]	hol min
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		b	[assert]	bool 1
Def		implies	[himplies]	hol min
Def		rep_prod	[hrep_prod]
Def		pair	[hpair]
Def		fst	[hfst]
Def		snd	[hsnd]
Def		uncurry	[huncurry]
Def		P & Q	[and]	core
Def		P  Q	[iff]	core
Def		mk_pair	[hmk_pair]
Def		x = y	[bequal]	hol
Def		pq	[band]	bool 1
Def		x:T. b(x)	[tlambda]	fun 1
Def			[bool]	bool 1
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		pq	[bimplies]	bool 1
Def		P	[prop_to_bool]	hol
Def		P  Q	[rev_implies]	core
Def		b	[bnot]	bool 1
Def		p  q	[bor]	bool 1
Def		@x:T. P(x)	[choose]	hol
Def		arb(T)	[arb]	hol

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