| 1996-01-30 | clasohm | expanded tabs | file | diff | annotate |
| 1995-05-01 | lcp | Simplified proof of Hausdorff_next_exists. | file | diff | annotate |
| 1994-12-19 | lcp | ran expandshort script | file | diff | annotate |
| 1994-12-16 | lcp | changed useless "qed" calls for lemmas back to uses of "result", | file | diff | annotate |
| 1994-12-07 | clasohm | added qed and qed_goal[w] | file | diff | annotate |
| 1994-09-09 | lcp | ZF/Zorn/next_bounded: deleted this proof, which was already in comments | file | diff | annotate |
| 1994-08-12 | lcp | installation of new inductive/datatype sections | file | diff | annotate |
| 1994-07-26 | lcp | Axiom of choice, cardinality results, etc. | file | diff | annotate |