Def		seq:l	[list_to_function]
Def		find_first_iter(v.p(v); v.f(v); a)	[find_first_iter]
Def		f is permutation on A	[is_permutation]
Def		fin_enum(A)	[fin_enum]
Def		Nil	[seq_nil]
Def		[x/ xs]	[seq_cons]
Def		xs	[list_member_type]
Def		1-1-Corr x:A,y:B. R(x;y)	[is_one_one_corr_rel]
Def		Prop	[prop]	core
Def		a -- b	[ndiff]	int 2
Def		AB	[isect_two]	LogicSupplement
Def		Finite(A)	[is_finite_type]
Def		Unbounded(A)	[unboundedly_infinite]
Def		Infinite(A)	[productively_infinite]
Def		a {k} T	[sized_mset]
Def		{i...}	[int_upper]	int 1
Def		a {k}	[sized_bool]
Def			[nat]	int 1
Def		{i..j}	[int_seg]	int 1
Def		{i...j}	[int_iseg]	int 1
Def		i  j < k	[lelt]	int 1
Def		AB	[le]	core
Def		IsEqFun(T;eq)	[eqfun_p]	rel 1
Def		A Discrete	[is_discrete]	LogicSupplement
Def		Dec(P)	[decidable]	core
Def		{a:T}	[singleton]	core
Def		A =ext B	[exteq]	LogicSupplement
Def		A bij B	[bijection_type]
Def		!A	[inhabited_uniquely]	LogicSupplement
Def		S  T	[subtype]	core
Def			[nat_plus]	int 1
Def		A onto B	[surjection_type]
Def		A & B	[cand]	core
Def		a  b	[nequal]	core
Def		1-1 xA,yB. R(x;y)	[rel_1_1_b]
Def		R is 1-1	[rel_1_1]
Def		SqStable(P)	[sq_stable]	core
Def		least i:. p(i)	[least]
Def		b	[assert]	bool 1
Def		x f y	[infix_ap]	core
Def		EquivRel on A, R	[equiv_rel_sep]	LogicSupplement
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		T	[squash]	core
Def		(x:A. B(x)) ~ (x':A'. B'(x'))	[one_one_corr_fams]
Def		union_to_sigma	[union_to_sigma]
Def		sigma_to_union	[sigma_to_union]
Def		k!	[factorial_via_iter]	IteratedBinops
Def		Dedekind-Infinite(A)	[Dedekind_infinite]
Def		x:A st P(x)B(x)	[fun_over_st]	LogicSupplement
Def		{T}	[guard]	core
Def		A/E	[quotient_sep]	LogicSupplement
Def		x:A st P(x). Q(x)	[allst]	LogicSupplement
Def		Unit	[unit]	core
Def		k!m	[factorial_tail_via_iter]	IteratedBinops
Def		prev_nat_pair	[prev_nat_pair]
Def		nat_to_nat_pair	[nat_to_nat_pair]
Def		same_range_sep(A; B)	[same_range_sep]
Def		!x:A. P(x)	[exists_unique]	LogicSupplement
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		P  Q	[or]	core
Def		False	[false]	core
Def		Y	[ycomb]	core
Def		if b t else f fi	[ifthenelse]	bool 1
Def		f{i}	[compose_iter]
Def		Replace value k by f(m) in f	[delete_fenum_value]
Def		next_nat_pair	[next_nat_pair]
Def		i=j	[eq_int]	bool 1
Def		P  Q	[iff]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[exists]	core
Def		AB	[inv_pair]
Def		A inj B	[injection_type]
Def		A	[inhabited]	LogicSupplement
Def		A	[not]	core
Def		size(a)	[boolsize]
Def		Msize	[msize]
Def		Iter(f;u) i:{a..b}. e(i)	[iter_via_intseg]	IteratedBinops
Def			[bool]	bool 1
Def		a  xs	[is_list_mem]
Def		A ~ B	[one_one_corr_2]
Def		A ~~ B	[one_one_corr]
Def		Replace values x s.t. P(x) by y in f	[replace_fn_values]
Def		InvFuns(A; B; f; g)	[inv_funs]
Def		Bij(A; B; f)	[biject]
Def		Inj(A; B; f)	[inject]
Def		Surj(A; B; f)	[surject]
Def		f is 1-1 corr	[is_one_one_corr]
Def		InvFuns(A;B;f;g)	[inv_funs_2]
Def		l[i]	[select]
Def		imax(a;b)	[imax]	int 2
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		1,2. b(1;2)	[so_lambda2]
Def		x is the u:A. P(u)	[is_the]	LogicSupplement
Def		P  Q	[rev_implies]	core
Def		nth_tl(n;as)	[nth_tl]
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		Id	[tidentity]
Def		f o g	[compose]
Def		hd(l)	[hd]
Def		Id	[identity]
Def		tl(l)	[tl]
Def		b	[bnot]	bool 1

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