Def		list_accum(x,a.f(x;a);y;l)	[list_accum]
Def		(x  l)	[l_member]
Def		last(L)	[last]
Def		x before y  l	[l_before]
Def		no_repeats(T;l)	[no_repeats]
Def		L1  L2	[sublist]
Def		l[i]	[select]	list 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		firstn(n;as)	[firstn]	list 1
Def		{i...j}	[int_iseg]	int 1
Def		ij	[ge]	core
Def			[nat]	int 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P  Q	[iff]	core
Def		Dec(P)	[decidable]	core
Def		Prop	[prop]	core
Def		tl(l)	[tl]	list 1
Def		hd(l)	[hd]	list 1
Def		Top	[top]	core
Def		{T}	[guard]	core
Def		mklist(n;f)	[mklist]
Def		False	[false]	core
Def		null(as)	[null]	list 1
Def		P  Q	[or]	core
Def		True	[true]	core
Def		A List	[listp]
Def			[bool]	bool 1
Def		pq	[band]	bool 1
Def		f o g	[compose]	fun 1
Def		l1  l2	[iseg]
Def		zip(as;bs)	[zip]
Def		unzip(as)	[unzip]
Def		(first x  as s.t. P(x) else d)	[find]
Def		as @ bs	[append]	list 1
Def		primrec(n;b;c)	[primrec]	mb nat
Def		||as||	[length]	list 1
Def		A & B	[cand]	core
Def		x:A. B(x)	[exists]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		b	[assert]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		filter(P;l)	[filter]
Def		reduce(f;k;as)	[reduce]	list 1
Def		Y	[ycomb]	core
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		map(f;as)	[map]	list 1
Def		A	[not]	core
Def		P  Q	[implies]	core
Def		P  Q	[rev_implies]	core
Def		i=j	[eq_int]	bool 1
Def		b	[bnot]	bool 1

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