Def		Prime	[prime_nats]
Def		is_prime(x)	[prime_decider]
Def		P & Q	[and]	core
Def		P  Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def		P  Q	[or]	core
Def		P  Q	[implies]	core
Def		{i...}	[int_upper]	int 1
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def			[nat]	int 1
Def		AB	[le]	core
Def			[nat_plus]	int 1
Def			[int_nzero]	int 1
Def		x:A. B(x)	[exists]	core
Def		prime(a)	[prime]	num thy 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def		Dec(P)	[decidable]	core
Def		a  b	[nequal]	core
Def		A	[not]	core
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		!A	[inhabited_uniquely]	LogicSupplement
Def		P  Q	[rev_implies]	core
Def		A	[inhabited]	LogicSupplement

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