| 1997-03-18 | paulson | Conducted the IFOL proofs using intuitionistic tools | file | diff | annotate |
| 1997-02-10 | paulson | Renamed structure Int (intuitionistic prover) to IntPr | file | diff | annotate |
| 1997-01-03 | paulson | Implicit simpsets and clasets for FOL and ZF | file | diff | annotate |
| 1996-01-30 | clasohm | expanded tabs | file | diff | annotate |
| 1994-12-20 | lcp | Used bind_thm to store domain_rel_subset and range_rel_subset | file | diff | annotate |
| 1994-12-07 | clasohm | added qed and qed_goal[w] | file | diff | annotate |
| 1994-11-24 | lcp | tidied proofs, using fast_tac etc. as much as possible | 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 |
| 1993-09-16 | clasohm | Initial revision | file | diff | annotate |