Def		A[P]	[type_if]
Def		bif(b; bx.x(bx); by.y(by))	[bif]
Def		isr(x)	[isr]
Def		type_tag(x;'a)	[type_tag]
Def		XM	[xmiddle]	core
Def		P	[prop_to_bool_2]
Def		Prop	[prop]	core
Def		S	[stype]
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		x:T. P(x)	[ball]
Def		x:T. P(x)	[bexists]
Def		False	[false]	core
Def		iso_pair('a;'b;P;rep;abs)	[iso_pair]
Def		ij	[le_int]	bool 1
Def		pq	[bimplies]	bool 1
Def		b	[bnot]	bool 1
Def		P  Q	[or]	core
Def		i<j	[lt_int]	bool 1
Def		{T}	[guard]	core
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		pq	[band]	bool 1
Def		eq('a)	[eq_pred]
Def		S  T	[subtype]	core
Def		<eq_pred:x>	[eq_pred_marker]
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		True	[true]	core
Def		x:A. B(x)	[exists]	core
Def		@x:T. P(x)	[choose]
Def		arb(T)	[arb]
Def		type_definition('a;'b;P;rep)	[type_definition]
Def		b	[assert]	bool 1
Def		x:A. B(x)	[all]	core
Def		x = y	[bequal]
Def		P	[prop_to_bool]
Def		if b t else f fi	[ifthenelse]	bool 1
Def		P  Q	[iff]	core
Def		P  Q	[implies]	core
Def		P & Q	[and]	core
Def		x:T. b(x)	[tlambda]	fun 1
Def			[bool]	bool 1
Def		p  q	[bor]	bool 1
Def		P  Q	[rev_implies]	core

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