Def		l_disjoint(T;l1;l2)	[l_disjoint]	mb list 2
Def		outl(x)	[outl]	union
Def		outr(x)	[outr]	union
Def		list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def		f[n:=x]	[fappend]	mb nat
Def		x,y,z. t(x;y;z)	[so_lambda3]	mb basic
Def		...	[hide]	mb basic
Def		ptn_int(x)	[ptn_int]	mb basic
Def		ptn_var(x)	[ptn_var]	mb basic
Def		lbl_pr( < x, y > )	[lbl_pair]	mb basic
Def		const_ptn(l)	[const_ptn]	mb basic
Def		int_ptn(l)	[int_ptn]	mb basic
Def		var_ptn(l)	[var_ptn]	mb basic
Def		left_ptn(l)	[left_ptn]	mb basic
Def		right_ptn(l)	[right_ptn]	mb basic
Def		ground_ptn(p)	[ground_ptn]	mb basic
Def		$x	[clbl]	mb basic
Def		StAntiSym(T;x,y.R(x;y))	[st_anti_sym]	rel 1
Def		Irrefl(T;x,y.E(x;y))	[irrefl]	rel 1
Def		For{T,op,id} x as. f(x)	[for]	list 1
Def		ForHdTl{A,f,k} h::t as. g(h;t)	[for_hdtl]	list 1
Def		mapc(f)	[mapc]	list 1
Def		t_iterate(l;n;t)	[t_iterate]	mb tree
Def		left_child(t)	[left_child]	mb tree
Def		right_child(t)	[right_child]	mb tree
Def		leaf_value(t)	[leaf_value]	mb tree
Def		tree_node( < x, y > )	[node]	mb tree
Def		Default = > body EndSwitch	[switch_default]	prog 1
Def		< x,y > = > body(x;y)	[case_pair]	prog 1
Def		x::y = > body(x;y) cont	[case_cons]	prog 1
Def		[] = > body cont	[case_nil]	prog 1
Def		= > body	[case_it]	prog 1
Def		x:body	[case_bind]	prog 1
Def		< < "a", b > , c, 1 > = > body(b;c) cont	[case_pattern1]	prog 1
Def		< a, inl < < "a", b > , c, 1 > > = > body(a;b;c) cont	[case_pattern2]	prog 1
Def		< a, inl < < "a", b > , c, 1 > >	[pattern2]	prog 1
Def		union1()	[union1]	prog 1
Def		union1_term1(x) = > body(x) cont	[case_union1_term1]	prog 1
Def		union1_term1(x)	[union1_term1]	prog 1
Def		union1_term2(x) = > body(x) cont	[case_union1_term2]	prog 1
Def		union1_term2(x)	[union1_term2]	prog 1
Def		union1_term3(x) = > body(x) cont	[case_union1_term3]	prog 1
Def		union1_term3(x)	[union1_term3]	prog 1
Def		enum1_switch(value;el1;el2;el3)	[enum1_switch]	prog 1
Def		enum1_el1 = > body cont	[case_enum1_el1]	prog 1
Def		enum1_el2 = > body cont	[case_enum1_el2]	prog 1
Def		enum1_el3 = > body cont	[case_enum1_el3]	prog 1
Def		module1_type(prop)	[module1_type]	prog 1
Def		t.tag	[module1_tag]	prog 1
Def		t.data	[module1_data]	prog 1
Def		module1(tag, data) = > body(tag;data)	[case_module1]	prog 1
Def		module1(tag, data)	[module1]	prog 1
Def		pq	[bxor]	bool 1
Def		pq	[rev_bimplies]	bool 1
Def		i j k	[lele]	int 1
Def		S T	[suptype]	int 1
Def		t ...$L	[label]	core
Def		???	[error]	core
Def		I	[icomb]	core
Def		K	[kcomb]	core
Def		S	[scomb]	core
Def		let x,y,z = a in t(x;y;z)	[spread3]	core
Def		let w,x,y,z = a in t(w;x;y;z)	[spread4]	core
Def		let a,b,c,d,e = u in v(a;b;c;d;e)	[spread5]	core
Def		let a,b,c,d,e,f = u in v(a;b;c;d;e;f)	[spread6]	core
Def		let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g)	[spread7]	core
Def		XM	[xmiddle]	core
Def		let x = a in b(x)	[let]	core
Def		[x]{T}	[type_inj]	core
Def		(first x as s.t. P(x) else d)	[find]	mb list 1
Def		(xL.P(x))	[l_all]	mb list 2
Def		agree_on_common(T;as;bs)	[agree_on_common]	mb list 1
Def		interleaving(T;L1;L2;L)	[interleaving]	mb list 2
Def		null(as)	[null]	list 1
Def		last(L)	[last]	mb list 1
Def		compose_flips(L)	[compose_flips]	mb list 2
Def		x before y l	[l_before]	mb list 1
Def		guarded_permutation(T;P)	[guarded_permutation]	mb list 2
Def		swap adjacent[P(x;y)]	[swap_adjacent]	mb list 2
Def		Bij(A; B; f)	[biject]	fun 1
Def		count(x < y in L | P(x;y))	[count_pairs]	mb list 1
Def		no_repeats(T;l)	[no_repeats]	mb list 2
Def		(xL.P(x))	[l_exists]	mb list 2
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def			[nat_plus]	int 1
Def		i = j	[pm_equal]	int 2
Def		|i|	[absval]	int 2
Def		Preorder(T;x,y.R(x;y))	[preorder]	rel 1
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		gcd(a;b)	[gcd]	num thy 1
Def		x:A. B(x)	[sq_exists]	core
Def		CoPrime(a,b)	[coprime]	num thy 1
Def		SqStable(P)	[sq_stable]	core
Def		atomic(a)	[atomic]	num thy 1
Def		prime(a)	[prime]	num thy 1
Def		a = b mod m	[eqmod]	num thy 1
Def		fib(n)	[fib]	num thy 1
Def		isl(x)	[isl]	union
Def		{i...j}	[int_iseg]	int 1
Def		ij	[ge]	core
Def		A List	[listp]	mb list 1
Def		l1 l2	[iseg]	mb list 1
Def		zip(as;bs)	[zip]	mb list 1
Def		unzip(as)	[unzip]	mb list 1
Def		sublist_occurence(T;L1;L2;f)	[sublist_occurence]	mb list 1
Def		interleaving_occurence(T;L1;L2;L;f1;f2)	[interleaving_occurence]	mb list 1
Def		nondecreasing(f;k)	[nondecreasing]	mb nat
Def		fadd(f;g)	[fadd]	mb nat
Def		R1 = > R2	[rel_implies]	mb nat
Def		R preserves P	[preserved_by]	mb nat
Def		R^-1	[rel_inverse]	mb nat
Def		R1 R2	[rel_or]	mb nat
Def		f^n	[fun_exp]	mb nat
Def		search(k;P)	[search]	mb nat
Def		P Q	[prop_and]	mb nat
Def		(ternary) R preserves P	[preserved_by2]	mb nat
Def		dec2bool(d)	[dec2bool]	mb basic
Def		Decision	[decision]	mb basic
Def		Pattern	[ptn]	mb basic
Def		SQType(T)	[sq_type]	sqequal 1
Def		l1 = l2	[eq_lbl]	mb basic
Def		Symmetrize(x,y.R(x;y);a;b)	[symmetrize]	rel 1
Def		IsEqFun(T;eq)	[eqfun_p]	rel 1
Def		strict_part(x,y.R(x;y);a;b)	[strict_part]	rel 1
Def		Linorder(T;x,y.R(x;y))	[linorder]	rel 1
Def		rev(as)	[reverse]	list 1
Def		as[m..n]	[segment]	list 1
Def		as\[i]	[reject]	list 1
Def		f{m..n}	[listify]	list 1
Def		A List(n)	[list_n]	list 1
Def		i > j	[gt]	core
Def		{...i}	[int_lower]	int 1
Def		imin(a;b)	[imin]	int 2
Def		a -- b	[ndiff]	int 2
Def		Rem(a;n;r)	[rem_nrel]	int 2
Def		a mod n	[modulus]	int 2
Def		a n	[div_floor]	int 2
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		{i...}	[int_upper]	int 1
Def		A ~~ B	[one_one_corr]	fun 1
Def		Tree(E)	[tree]	mb tree
Def		tree_leaf(x)	[tree_leaf]	mb tree
Def		is_leaf(t)	[is_leaf]	mb tree
Def		enum1()	[enum1]	prog 1
Def		b2i(b)	[b2i]	bool 1
Def		p=q	[eq_bool]	bool 1
Def		Stable{P}	[stable]	core
Def		{a:T}	[singleton]	core
Def		{!x:T | P(x)}	[unique_set]	core
Def		a = !x:T. Q(x)	[uni_sat]	core
Def		(x l)	[l_member]	mb list 1
Def		P Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		disjoint_sublists(T;L1;L2;L)	[disjoint_sublists]	mb list 1
Def		swap(L;i;j)	[swap]	mb list 2
Def		(L o f)	[permute_list]	mb list 2
Def		L1 L2	[sublist]	mb list 1
Def		||as||	[length]	list 1
Def		R^*	[rel_star]	mb nat
Def			[nat]	int 1
Def		l[i]	[select]	list 1
Def		mklist(n;f)	[mklist]	mb list 1
Def		(i, j)	[flip]	mb nat
Def		map(f;as)	[map]	list 1
Def		compose_list(L)	[compose_list]	mb list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def		reducible(a)	[reducible]	num thy 1
Def			[int_nzero]	int 1
Def		Div(a;n;q)	[div_nrel]	int 2
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		a b	[nequal]	core
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		filter(P;l)	[filter]	mb list 1
Def		GCD(a;b;y)	[gcd_p]	num thy 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def		sum(f(x;y) | x < n; y < m)	[double_sum]	mb nat
Def		sum(f(x) | x < k)	[sum]	mb nat
Def		primrec(n;b;c)	[primrec]	mb nat
Def		rel_exp(T;R;n)	[rel_exp]	mb nat
Def		Case v = > case cont	[switch_case]	prog 1
Def		i=j	[eq_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def		P Q	[or]	core
Def		pq	[bimplies]	bool 1
Def		p q	[bor]	bool 1
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		as @ bs	[append]	list 1
Def		A & B	[cand]	core
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		imax(a;b)	[imax]	int 2
Def		ij	[le_int]	bool 1
Def		firstn(n;as)	[firstn]	list 1
Def		i < j	[lt_int]	bool 1
Def		b	[assert]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		2of(t)	[pi2]	core
Def		1of(t)	[pi1]	core
Def		pq	[band]	bool 1
Def		InvFuns(A; B; f; g)	[inv_funs]	fun 1
Def		f o g	[compose]	fun 1
Def		True	[true]	core
Def		x f y	[infix_ap]	core
Def		Top	[top]	core
Def		Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def		Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def		tl(l)	[tl]	list 1
Def		hd(l)	[hd]	list 1
Def		inl(x) = > body(x) cont	[case_inl]	prog 1
Def		inr(x) = > body(x) cont	[case_inr]	prog 1
Def		ptn_con(T)	[ptn_con]	mb basic
Def		ptn_pr(x)	[ptn_pr]	mb basic
Def		Default = > body	[case_default]	prog 1
Def		Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def		Case(value) body	[case]	prog 1
Def		Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def		x=yAtom	[eq_atom]	bool 1
Def		ptn_atom(x)	[ptn_atom]	mb basic
Def		Order(T;x,y.R(x;y))	[order]	rel 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		P Q	[iff]	core
Def		AntiSym(T;x,y.R(x;y))	[anti_sym]	rel 1
Def		Connex(T;x,y.R(x;y))	[connex]	rel 1
Def		x:T. b(x)	[tlambda]	fun 1
Def		mapcons(f;as)	[mapcons]	list 1
Def		Id	[tidentity]	fun 1
Def		Id	[identity]	fun 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		tree_con(E;T)	[tree_con]	mb tree
Def		Case tree_leaf(x) = > body(x) cont	[case_tree_leaf]	mb tree
Def		Case x;y = > body(x;y) cont	[case_node]	mb tree
Def		tree_node(x)	[tree_node]	mb tree
Def		< < "a", b > , c, 1 >	[pattern1]	prog 1
Def			[bool]	bool 1
Def		EndSwitch	[switch_done]	prog 1
Def		enum1_el3	[enum1_el3]	prog 1
Def		enum1_el2	[enum1_el2]	prog 1
Def		enum1_el1	[enum1_el1]	prog 1
Def		Switch(t) b	[switch]	prog 1
Def		Unit	[unit]	core
Def		{T}	[guard]	core
Def			[it]	core
Def		False	[false]	core
Def		b	[bnot]	bool 1
Def		S T	[subtype]	core
Def		Prop	[prop]	core
Def		P Q	[rev_implies]	core
Def		T	[squash]	core

About: