mb list 2	More list stuff from Mark Bickford.
mb list 1	Filter, initial-segment, list-member, interleaving, etc. Lemmas related to map, append, cons, select.
mb nat	Material pertaining to natural numbers as opposed to integers generally.
mb basic	Basic generally useful devices.
sqequal 1
list 1
fun 1
num thy 1	Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven.
rel 1	Common properties of binary relations.
union	Non canonical functions (isl, outl, outr) for union type.
int 2
bool 1
int 1
well fnd
core	Some basic concepts defined type-theoretically.