Def		type_definition	[htype_definition]	hol bool
Def		exists	[hexists]	hol bool
Def		select	[hselect]	hol min
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		exists_unique	[hexists_unique]	hol bool
Def		x:T. b(x)	[tlambda]	fun 1
Def		hbool	[hbool]	hol min
Def		hone	[hone]
Def		'a  'b	[hfun]	hol min
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		b_exists_unique('a;x.p(x))	[b_exists_unique]	hol bool
Def		x:T. P(x)	[bexists]	hol
Def		@x:'a. p(x)	[bchoose]	hol min
Def		x:T. P(x)	[ball]	hol
Def		b	[assert]	bool 1
Def		t	[ht]	hol bool
Def		one_el	[hone_el]
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[exists]	core
Def		P & Q	[and]	core
Def		Unit	[unit]	core
Def			[it]	core
Def		x = y	[bequal]	hol
Def		P	[prop_to_bool]	hol
Def		P  Q	[iff]	core
Def		@x:T. P(x)	[choose]	hol
Def		pq	[band]	bool 1
Def		pq	[bimplies]	bool 1
Def		P  Q	[rev_implies]	core
Def		arb(T)	[arb]	hol
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