| HOLlib | Doug Howe's HOL library. |
| hol one | |
| hol arithmetic 5 | |
| hol arithmetic 4 | |
| hol arithmetic 3 | |
| hol arithmetic 2 | |
| hol list 2 | |
| hol list 1 | |
| hol restr binder | |
| hol arithmetic 1 | |
| hol prim rec | |
| hol pair | |
| hol num | |
| list 1 | |
| int 2 | |
| hol sum | |
| hol combin | |
| hol bool | |
| hol min | |
| hol | |
| union | Non canonical functions (isl, outl, outr) for union type. |
| bool 1 | |
| int 1 | |
| well fnd | |
| fun 1 | |
| core | Some basic concepts defined type-theoretically. |