| MarkB generic | Mark Bickford's generic formal devices. |
| mb list 2 | More list stuff from Mark Bickford. |
| num thy 1 | Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven. |
| union | Non canonical functions (isl, outl, outr) for union type. |
| 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. |
| rel 1 | Common properties of binary relations. |
| list 1 | |
| int 2 | |
| fun 1 | |
| mb tree | Binary Trees (Mark Bickford) |
| prog 1 | |
| sqequal 1 | |
| bool 1 | |
| int 1 | |
| well fnd | |
| core | Some basic concepts defined type-theoretically. |