Def		x:T. b(x)	[tlambda]
Def		SqStable(P)	[sq_stable]	core
Def		Prop	[prop]	core
Def		Bij(A; B; f)	[biject]
Def		A ~~ B	[one_one_corr]
Def		P  Q	[iff]	core
Def		InvFuns(A; B; f; g)	[inv_funs]
Def		Id	[tidentity]
Def		Id	[identity]
Def		f o g	[compose]
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		Surj(A; B; f)	[surject]
Def		Inj(A; B; f)	[inject]
Def		T	[squash]	core
Def		P  Q	[rev_implies]	core

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