Def		pq	[bxor]
Def		pq	[rev_bimplies]
Def			[bool]
Def		x:A. B(x)	[all]	core
Def		b2i(b)	[b2i]
Def		{i..j}	[int_seg]	int 1
Def			[nat]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P & Q	[and]	core
Def		Dec(P)	[decidable]	core
Def		a  b	[nequal]	core
Def		A	[not]	core
Def		P  Q	[or]	core
Def		{T}	[guard]	core
Def		P  Q	[implies]	core
Def		Prop	[prop]	core
Def		ij	[le_int]
Def		b	[assert]
Def		P  Q	[iff]	core
Def		x=yAtom	[eq_atom]
Def		i=j	[eq_int]
Def		p=q	[eq_bool]
Def		Unit	[unit]	core
Def			[it]	core
Def		False	[false]	core
Def		True	[true]	core
Def		if b t else f fi	[ifthenelse]
Def		true	[btrue]
Def		false	[bfalse]
Def		pq	[bimplies]
Def		b	[bnot]
Def		pq	[band]
Def		p  q	[bor]
Def		i<j	[lt_int]
Def		P  Q	[rev_implies]	core

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