Def		f[n:=x]	[fappend]
Def		(ternary) R preserves P	[preserved_by2]
Def		increasing(f;k)	[increasing]	mb basic
Def		{T}	[guard]	core
Def		Bij(A; B; f)	[biject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		nondecreasing(f;k)	[nondecreasing]
Def		Dec(P)	[decidable]	core
Def		R^*	[rel_star]
Def		{i..j}	[int_seg]	int 1
Def			[nat]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		A	[not]	core
Def		fadd(f;g)	[fadd]
Def		Prop	[prop]	core
Def			[bool]	bool 1
Def		A & B	[cand]	core
Def		l[i]	[select]	list 1
Def		i>j	[gt]	core
Def		||as||	[length]	list 1
Def		sum(f(x;y) | x < n; y < m)	[double_sum]
Def		R1 => R2	[rel_implies]
Def		R preserves P	[preserved_by]
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		R^-1	[rel_inverse]
Def		P  Q	[iff]	core
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		R1  R2	[rel_or]
Def		f^n	[fun_exp]
Def			[nat_plus]	int 1
Def		(i, j)	[flip]
Def		search(k;P)	[search]
Def		b	[assert]	bool 1
Def		P  Q	[prop_and]
Def		sum(f(x) | x < k)	[sum]
Def		primrec(n;b;c)	[primrec]
Def		R^n	[rel_exp]
Def		i=j	[eq_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def		x:A. B(x)	[all]	core
Def		x f y	[infix_ap]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		P  Q	[implies]	core
Def		P  Q	[or]	core
Def		f o g	[compose]	fun 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		hd(l)	[hd]	list 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		P  Q	[rev_implies]	core
Def		tl(l)	[tl]	list 1
Def		b	[bnot]	bool 1

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