Def		union-reduce(f;g;x;as)	[union-reduce]
Def		< x,y > .P(x;y)	[plambda]
Def		l_disjoint(T;l1;l2)	[l_disjoint]	mb list 2
Def		(x l)	[l_member]	mb list 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 2
Def		l[i]	[select]	list 1
Def		||as||	[length]	list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def		(xL.P(x))	[l_ball]
Def		b	[assert]	bool 1
Def		P Q	[iff]	core
Def			[bool]	bool 1
Def		x:A. B(x)	[all]	core
Def		x:A. B(x)	[exists]	core
Def		(xL.P(x))	[l_bexists]
Def		P & Q	[and]	core
Def		rev(as)	[reverse]	list 1
Def		as @ bs	[append]	list 1
Def			[nat]	int 1
Def		{i...j}	[int_iseg]	int 1
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P Q	[implies]	core
Def		{T}	[guard]	core
Def		upto(i;j)	[upto]
Def		Dec(P)	[decidable]	core
Def		InvFuns(A; B; f; g)	[inv_funs]	fun 1
Def		f o g	[compose]	fun 1
Def		(f1,f2) o g	[compose2]
Def		Id	[tidentity]	fun 1
Def		Id	[identity]	fun 1
Def		Bij(A; B; f)	[biject]	fun 1
Def		firstn(n;as)	[firstn]	list 1
Def		mapoutl(s)	[mapoutl]
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def		map(f;as)	[map]	list 1
Def		Top	[top]	core
Def		nth_tl(n;as)	[nth_tl]	list 1
Def			[int_nzero]	int 1
Def		a b	[nequal]	core
Def		A	[not]	core
Def		P Q	[or]	core
Def		process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; }	[accumulate]
Def		Prop	[prop]	core
Def		sum(f(x) | x < k)	[sum]	mb nat
Def		primrec(n;b;c)	[primrec]	mb nat
Def		filter(P;l)	[filter]	mb list 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		A & B	[cand]	core
Def		|i|	[absval]	int 2
Def		f91(i)	[f91]
Def		i > j	[gt]	core
Def		a mod n	[modulus]	int 2
Def		a n	[div_floor]	int 2
Def			[nat_plus]	int 1
Def		i=j	[eq_int]	bool 1
Def		true	[btrue]	bool 1
Def		pq	[band]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		false	[bfalse]	bool 1
Def		p q	[bor]	bool 1
Def		ij	[le_int]	bool 1
Def		i < j	[lt_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def		isl(x)	[isl]	union
Def		outl(x)	[outl]	union
Def		hd(l)	[hd]	list 1
Def		P Q	[rev_implies]	core
Def		Surj(A; B; f)	[surject]	fun 1
Def		tl(l)	[tl]	list 1
Def		b	[bnot]	bool 1

About: