Def		nnsub(m;n)	[nnsub]	hol arithmetic 1
Def		P & Q	[and]	core
Def			[nat]	int 1
Def		x:A. B(x)	[all]	core
Def		P  Q	[implies]	core
Def		AB	[le]	core
Def		A	[not]	core
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		S	[stype]	hol
Def		P  Q	[iff]	core
Def		P  Q	[or]	core
Def		pre(n)	[pre]	hol prim rec
Def		x:A. B(x)	[exists]	core
Def		exp(m;n)	[exp]	hol arithmetic 1
Def		nmod(m;n)	[nmod]	hol arithmetic 1
Def		ndiv(m;n)	[ndiv]	hol arithmetic 1
Def		i<j	[lt_int]	bool 1
Def		bif(b; bx.x(bx); by.y(by))	[bif]	hol
Def		P  Q	[rev_implies]	core
Def		i=j	[eq_int]	bool 1

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