Def	Label	[lbl]
Def	x:A. B(x)	[all]	core
Def	P Q	[implies]	core
Def	SQType(T)	[sq_type]	sqequal 1
Def	P Q	[iff]	core
Def	(x l)	[l_member]	mb list 1
Def	x ls	[lbls_member]
Def	Dec(P)	[decidable]	core
Def	ground_ptn(p)	[ground_ptn]	mb basic
Def	b	[assert]	bool 1
Def	Pattern	[ptn]	mb basic
Def	false	[bfalse]	bool 1
Def	l1 = l2	[eq_lbl]	mb basic
Def	p q	[bor]	bool 1
Def	reduce(f;k;as)	[reduce]	list 1
Def	P Q	[rev_implies]	core
Def	l[i]	[select]	list 1
Def	||as||	[length]	list 1
Def		[nat]	int 1
Def	AB	[le]	core
Def	A	[not]	core
Def	Default = > body	[case_default]	prog 1
Def	pq	[band]	bool 1
Def	Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def	Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def	Case(value) body	[case]	prog 1
Def	ptn_con(T)	[ptn_con]	mb basic
Def	x=yAtom	[eq_atom]	bool 1
Def	i=j	[eq_int]	bool 1
Def	Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def	Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def	nth_tl(n;as)	[nth_tl]	list 1
Def	hd(l)	[hd]	list 1
Def	tl(l)	[tl]	list 1
Def	inl(x) = > body(x) cont	[case_inl]	prog 1
Def	inr(x) = > body(x) cont	[case_inr]	prog 1
Def	ij	[le_int]	bool 1
Def	i < j	[lt_int]	bool 1
Def	b	[bnot]	bool 1

About: