Def		P  Q	[iff]	core
Def			[nat]	int 1
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def			[nat_plus]	int 1
Def		i =  j	[pm_equal]	int 2
Def		|i|	[absval]	int 2
Def		Preorder(T;x,y.R(x;y))	[preorder]	rel 1
Def		Dec(P)	[decidable]	core
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		gcd(a;b)	[gcd]
Def		x:A. B(x)	[sq_exists]	core
Def		CoPrime(a,b)	[coprime]
Def		SqStable(P)	[sq_stable]	core
Def		{T}	[guard]	core
Def		atomic(a)	[atomic]
Def		prime(a)	[prime]
Def		a = b mod m	[eqmod]
Def		fib(n)	[fib]
Def		x:A. B(x)	[exists]	core
Def		GCD(a;b;y)	[gcd_p]
Def		reducible(a)	[reducible]
Def		a ~ b	[assoced]
Def		b | a	[divides]
Def		P & Q	[and]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		i=j	[eq_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def			[int_nzero]	int 1
Def		a  b	[nequal]	core
Def		A	[not]	core
Def		P  Q	[or]	core
Def		p  q	[bor]	bool 1
Def		P  Q	[rev_implies]	core
Def		ij	[le_int]	bool 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		T	[squash]	core
Def		i<j	[lt_int]	bool 1
Def		b	[bnot]	bool 1

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