Def		outl(x)	[outl]	union
Def		outl	[houtl]
Def		exists	[hexists]	hol bool
Def		is_sum_rep	[his_sum_rep]
Def		all	[hall]	hol bool
Def		type_definition	[htype_definition]	hol bool
Def		exists_unique	[hexists_unique]	hol bool
Def		b_exists_unique('a;x.p(x))	[b_exists_unique]	hol bool
Def		x:T. P(x)	[bexists]	hol
Def		x:T. P(x)	[ball]	hol
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		b	[assert]	bool 1
Def		P  Q	[implies]	core
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def		outr(x)	[outr]	union
Def		outr	[houtr]
Def		hsum('a; 'b)	[hsum]
Def		not	[hnot]	hol bool
Def		and	[hand]	hol bool
Def		or	[hor]	hol bool
Def		equal	[hequal]	hol min
Def		hbool	[hbool]	hol min
Def		'a  'b	[hfun]	hol min
Def		abs_sum	[habs_sum]
Def		P & Q	[and]	core
Def		inl	[hinl]
Def		inr	[hinr]
Def		isl	[hisl]
Def		isr	[hisr]
Def		o	[ho]	hol combin
Def		implies	[himplies]	hol min
Def		f o g	[compose]	fun 1
Def		x:A. B(x)	[exists]	core
Def		P  Q	[or]	core
Def		rep_sum	[hrep_sum]
Def		pq	[bimplies]	bool 1
Def		b	[bnot]	bool 1
Def		x = y	[bequal]	hol
Def		pq	[band]	bool 1
Def			[bool]	bool 1
Def		x:T. b(x)	[tlambda]	fun 1
Def		@x:T. P(x)	[choose]	hol
Def		isl(x)	[isl]	union
Def		isr(x)	[isr]	hol
Def		arb(T)	[arb]	hol
Def		p  q	[bor]	bool 1
Def		P	[prop_to_bool]	hol
Def		P  Q	[iff]	core
Def		P  Q	[rev_implies]	core

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