Def		zero	[hzero]
Def		i>j	[gt]	core
Def		P  Q	[implies]	core
Def		Dec(P)	[decidable]	core
Def		iso_pair('a;'b;P;rep;abs)	[iso_pair]	hol
Def		type_definition	[htype_definition]	hol bool
Def		type_definition('a;'b;P;rep)	[type_definition]	hol
Def		P  Q	[iff]	core
Def		abs_num	[habs_num]
Def		hnum	[hnum]
Def		hind	[hind]	hol min
Def		'a  'b	[hfun]	hol min
Def		is_num_rep	[his_num_rep]
Def		onto	[honto]	hol bool
Def		not	[hnot]	hol bool
Def		one_one	[hone_one]	hol bool
Def		and	[hand]	hol bool
Def		select	[hselect]	hol min
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		exists	[hexists]	hol bool
Def		x:T. P(x)	[ball]	hol
Def		@x:'a. p(x)	[bchoose]	hol min
Def		x:T. P(x)	[bexists]	hol
Def		b	[assert]	bool 1
Def		implies	[himplies]	hol min
Def		hbool	[hbool]	hol min
Def		suc	[hsuc]
Def		rep_num	[hrep_num]
Def		ncompose(f;n;x)	[ncompose]
Def		i=j	[eq_int]	bool 1
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		Y	[ycomb]	core
Def		zero_rep	[hzero_rep]
Def		suc_rep	[hsuc_rep]
Def			[nat]	int 1
Def		onto('a;'b;f)	[onto]	hol bool
Def		AB	[le]	core
Def		A	[not]	core
Def		one_one('a;'b;f)	[one_one]	hol bool
Def		P & Q	[and]	core
Def		@x:T. P(x)	[choose]	hol
Def		x:T. b(x)	[tlambda]	fun 1
Def		x:A. B(x)	[all]	core
Def		pq	[band]	bool 1
Def		pq	[bimplies]	bool 1
Def			[bool]	bool 1
Def		P  Q	[rev_implies]	core
Def		x = y	[bequal]	hol
Def		P	[prop_to_bool]	hol
Def		b	[bnot]	bool 1
Def		arb(T)	[arb]	hol
Def		p  q	[bor]	bool 1

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