Def		{i..j}	[int_seg]	int 1
Def		x:A. B(x)	[exists]	core
Def			[nat_plus]	int 1
Def			[nat]	int 1
Def		x:A. B(x)	[all]	core
Def		fib(n)	[fib]	num thy 1
Def		CoPrime(a,b)	[coprime]	num thy 1
Def		GCD(a;b;y)	[gcd_p]	num thy 1
Def		{i...}	[int_upper]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		i=j	[eq_int]	bool 1
Def		p  q	[bor]	bool 1
Def		b | a	[divides]	num thy 1

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