Def		l_disjoint(T;l1;l2)	[l_disjoint]
Def		(xL.P(x))	[l_all]
Def		P  Q	[iff]	core
Def		Prop	[prop]	core
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		true	[btrue]	bool 1
Def		x before y  l	[l_before]	mb list 1
Def		L1  L2	[sublist]	mb list 1
Def		no_repeats(T;l)	[no_repeats]	mb list 1
Def		Dec(P)	[decidable]	core
Def		False	[false]	core
Def		(xL.P(x))	[l_exists]
Def		P  Q	[or]	core
Def		mapfilter(f;P;L)	[mapfilter]
Def		A & B	[cand]	core
Def		sublist_occurence(T;L1;L2;f)	[sublist_occurence]
Def		{T}	[guard]	core
Def		interleaving(T;L1;L2;L)	[interleaving]
Def		interleaving_occurence(T;L1;L2;L;f1;f2)	[interleaving_occurence]
Def		guarded_permutation(T;P)	[guarded_permutation]
Def		l1  l2	[iseg]	mb list 1
Def		swap adjacent[P(x;y)]	[swap_adjacent]
Def		swap(L;i;j)	[swap]
Def		(L o f)	[permute_list]
Def		mklist(n;f)	[mklist]	mb list 1
Def		as @ bs	[append]	list 1
Def		x f y	[infix_ap]	core
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		count(x < y in L | P(x;y))	[count_pairs]
Def		Bij(A; B; f)	[biject]	fun 1
Def		last(L)	[last]	mb list 1
Def		R^*	[rel_star]	mb nat
Def		R^n	[rel_exp]	mb nat
Def		compose_flips(L)	[compose_flips]
Def		sum(f(x;y) | x < n; y < m)	[double_sum]	mb nat
Def		sum(f(x) | x < k)	[sum]	mb nat
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		(x  l)	[l_member]	mb list 1
Def		P & Q	[and]	core
Def		disjoint_sublists(T;L1;L2;L)	[disjoint_sublists]
Def		increasing(f;k)	[increasing]	mb basic
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		x:A. B(x)	[all]	core
Def		P  Q	[implies]	core
Def		x:A. B(x)	[exists]	core
Def		filter(P;l)	[filter]	mb list 1
Def		map(f;as)	[map]	list 1
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		(i, j)	[flip]	mb nat
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		ij	[le_int]	bool 1
Def		i<j	[lt_int]	bool 1
Def		pq	[band]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		compose_list(L)	[compose_list]
Def		f o g	[compose]	fun 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		P  Q	[rev_implies]	core
Def		Surj(A; B; f)	[surject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		primrec(n;b;c)	[primrec]	mb nat
Def		i=j	[eq_int]	bool 1
Def		hd(l)	[hd]	list 1
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