Def		a  b	[nequal]
Def		x:A. B(x)	[sq_exists]
Def		ij	[ge]
Def		i>j	[gt]
Def		S  T	[subtype]
Def		Top	[top]
Def		x f y	[infix_ap]
Def		t  ...$L	[label]
Def		???	[error]
Def		A & B	[cand]
Def		I	[icomb]
Def		K	[kcomb]
Def		S	[scomb]
Def		let x,y,z = a in t(x;y;z)	[spread3]
Def		let w,x,y,z = a in t(w;x;y;z)	[spread4]
Def		let a,b,c,d,e = u in v(a;b;c;d;e)	[spread5]
Def		let a,b,c,d,e,f = u in v(a;b;c;d;e;f)	[spread6]
Def		let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g)	[spread7]
Def		XM	[xmiddle]
Def		let x = a in b(x)	[let]
Def		[x]{T}	[type_inj]
Def		Y	[ycomb]
Def		2of(t)	[pi2]
Def		1of(t)	[pi1]
Def			[it]
Def		Unit	[unit]
Def		P  Q	[iff]
Def		Stable{P}	[stable]
Def		SqStable(P)	[sq_stable]
Def		{T}	[guard]
Def		x:A. B(x)	[exists]
Def		{a:T}	[singleton]
Def		{!x:T | P(x)}	[unique_set]
Def		a = !x:T. Q(x)	[uni_sat]
Def		P  Q	[implies]
Def		True	[true]
Def		False	[false]
Def		AB	[le]
Def		Dec(P)	[decidable]
Def		A	[not]
Def		P  Q	[rev_implies]
Def		P & Q	[and]
Def		x:A. B(x)	[all]
Def		P  Q	[or]
Def		T	[squash]
Def		Prop	[prop]

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