core_1
canonical form tests
isect_1
core_2
well_fnd
subtype_0
sqequal_1
basic_types
union
atom_1
call by value_1
arithmetic
computation
call by value_2
bar-induction
per type 1
per type
bool_1
int_1
fun_1
subtype_1
ppcc
rel_1
relations
equality deciders
quot_1
per-quotient
partial_1
dependent intersection
co-recursion
list_0
ML
omega
co-recursion-2
int_2
list_1
integer polynomials
rec_values
decidable equality
finite sets
relations2
terms
spread
tuples
equipollence (cardinality)
num_thy_1
fan-theorem
prog_1
continuity
Home
Index