Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		P  Q	[implies]	core
Def		Prop	[prop]	core
Def		x:A. B(x)	[all]	core
Def		S  T	[subtype]	core
Def		SqStable(P)	[sq_stable]	core
Def		T	[squash]	core
Def		P  Q	[iff]	core
Def		x f y	[infix_ap]	core
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		x:A. B(x)	[exists]	core
Def		Dec(P)	[decidable]	core
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		P  Q	[rev_implies]	core
Def		A	[not]	core

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