Def		StAntiSym(T;x,y.R(x;y))	[st_anti_sym]
Def		Irrefl(T;x,y.E(x;y))	[irrefl]
Def		Prop	[prop]	core
Def		{T}	[guard]	core
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]
Def		Symmetrize(x,y.R(x;y);a;b)	[symmetrize]
Def		Preorder(T;x,y.R(x;y))	[preorder]
Def		SqStable(P)	[sq_stable]	core
Def		T	[squash]	core
Def		IsEqFun(T;eq)	[eqfun_p]
Def			[bool]	bool 1
Def		strict_part(x,y.R(x;y);a;b)	[strict_part]
Def		Dec(P)	[decidable]	core
Def		Linorder(T;x,y.R(x;y))	[linorder]
Def		x:A. B(x)	[all]	core
Def		P  Q	[implies]	core
Def		Order(T;x,y.R(x;y))	[order]
Def		Trans x,y:T. E(x;y)	[trans]
Def		Sym x,y:T. E(x;y)	[sym]
Def		Refl(T;x,y.E(x;y))	[refl]
Def		P & Q	[and]	core
Def		x f y	[infix_ap]	core
Def		b	[assert]	bool 1
Def		P  Q	[iff]	core
Def		A	[not]	core
Def		P  Q	[or]	core
Def		AntiSym(T;x,y.R(x;y))	[anti_sym]
Def		Connex(T;x,y.R(x;y))	[connex]
Def		P  Q	[rev_implies]	core

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