Def		add	[hadd]
Def		sub	[hsub]
Def		mult	[hmult]
Def		exp	[hexp]
Def		gt	[hgt]
Def		le	[hle]
Def		ge	[hge]
Def		fact	[hfact]
Def		even	[heven]
Def		odd	[hodd]
Def		mod	[hmod]
Def		div	[hdiv]
Def		x:A. B(x)	[all]	core
Def			[nat]	int 1
Def		AB	[le]	core
Def		P  Q	[implies]	core
Def		i>j	[gt]	core
Def			[bool]	bool 1
Def		nnsub(m;n)	[nnsub]
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		exp(m;n)	[exp]
Def		fact(n)	[fact]
Def		even(n)	[even]
Def		odd(n)	[odd]
Def		nmod(m;n)	[nmod]
Def		ndiv(m;n)	[ndiv]
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		i=j	[eq_int]	bool 1
Def		Y	[ycomb]	core
Def		b	[bnot]	bool 1
Def		true	[btrue]	bool 1
Def		false	[bfalse]	bool 1
Def		x:T. b(x)	[tlambda]	fun 1
Def		A	[not]	core

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