Def		Prop	[prop]	core
Def		P  Q	[implies]	core
Def			[nat]	int 1
Def		is_assoc_sep(A; f)	[is_assoc_sep]
Def		{i...}	[int_upper]	int 1
Def		{...i}	[int_lower]	int 1
Def		{T}	[guard]	core
Def		{i...j}	[int_iseg]	int 1
Def		i  j  k	[lele]	int 1
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P  Q	[or]	core
Def		b | a	[divides]	num thy 1
Def		P  Q	[iff]	core
Def		True	[true]	core
Def		x:A. B(x)	[exists]	core
Def		A	[not]	core
Def		False	[false]	core
Def		k!	[factorial_via_iter]
Def			[nat_plus]	int 1
Def		P & Q	[and]	core
Def		x:A. B(x)	[all]	core
Def		is_assoc(A; x,z.f(x;z))	[is_assoc]
Def		is_commutative_sep(A; f)	[is_commutative_sep]
Def		is_commutative(A; x,z.f(x;z))	[is_commutative]
Def		k!m	[factorial_tail_via_iter]
Def		Iter(f;u) i:{a..b}. e(i)	[iter_via_intseg]
Def		i<j	[lt_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def		is_ident(A; f; u)	[is_ident]
Def		P  Q	[rev_implies]	core

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