Def		suc	[hsuc]	hol num
Def		add	[hadd]	hol arithmetic 1
Def		equal	[hequal]	hol min
Def		all	[hall]	hol bool
Def		and	[hand]	hol bool
Def		lt	[hlt]	hol prim rec
Def		cond	[hcond]	hol bool
Def		sub	[hsub]	hol arithmetic 1
Def		mult	[hmult]	hol arithmetic 1
Def		exp	[hexp]	hol arithmetic 1
Def		gt	[hgt]	hol arithmetic 1
Def		or	[hor]	hol bool
Def		le	[hle]	hol arithmetic 1
Def		ge	[hge]	hol arithmetic 1
Def		fact	[hfact]	hol arithmetic 1
Def		not	[hnot]	hol bool
Def		even	[heven]	hol arithmetic 1
Def		odd	[hodd]	hol arithmetic 1
Def		mod	[hmod]	hol arithmetic 1
Def		div	[hdiv]	hol arithmetic 1
Def		implies	[himplies]	hol min
Def		exists	[hexists]	hol bool
Def		pre	[hpre]	hol prim rec
Def		x:T. b(x)	[tlambda]	fun 1
Def		hnum	[hnum]	hol num
Def		x:T. P(x)	[ball]	hol
Def		x:T. P(x)	[bexists]	hol
Def		b	[assert]	bool 1
Def		hbool	[hbool]	hol min
Def		t	[ht]	hol bool
Def		f	[hf]	hol bool
Def		'a  'b	[hfun]	hol min
Def		S	[stype]	hol
Def		x:A. B(x)	[all]	core
Def			[nat]	int 1
Def		x = y	[bequal]	hol
Def		pq	[band]	bool 1
Def		nnsub(m;n)	[nnsub]	hol arithmetic 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		exp(m;n)	[exp]	hol arithmetic 1
Def		fact(n)	[fact]	hol arithmetic 1
Def		even(n)	[even]	hol arithmetic 1
Def		odd(n)	[odd]	hol arithmetic 1
Def		nmod(m;n)	[nmod]	hol arithmetic 1
Def		ndiv(m;n)	[ndiv]	hol arithmetic 1
Def		pre(n)	[pre]	hol prim rec
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		pq	[bimplies]	bool 1
Def		p  q	[bor]	bool 1
Def		b	[bnot]	bool 1
Def		AB	[le]	core
Def		P	[prop_to_bool]	hol
Def		i=j	[eq_int]	bool 1
Def		A	[not]	core

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