Def		exp(m;n)	[exp]	hol arithmetic 1
Def			[nat]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		x:A. B(x)	[all]	core
Def		P  Q	[or]	core
Def		x:A. B(x)	[exists]	core
Def		True	[true]	core
Def		P  Q	[implies]	core
Def		P  Q	[iff]	core
Def		P & Q	[and]	core
Def		fact(n)	[fact]	hol arithmetic 1
Def		odd(n)	[odd]	hol arithmetic 1
Def		even(n)	[even]	hol arithmetic 1
Def		b	[assert]	bool 1
Def		ij	[le_int]	bool 1
Def		nnsub(m;n)	[nnsub]	hol arithmetic 1
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		i=j	[eq_int]	bool 1
Def		P  Q	[rev_implies]	core
Def		b	[bnot]	bool 1
Def		i<j	[lt_int]	bool 1

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