2005-05-22 | wenzelm | Simplifier already setup in Pure; | file | diff | annotate |
2002-11-28 | ballarin | Transitivity reasoner renamed to linorder.ML. README updated. | file | diff | annotate |
2002-11-28 | ballarin | HOL-Algebra partially ported to Isar. | file | diff | annotate |
2001-10-19 | wenzelm | induct_method.ML -- proof by cases and induction on sets and types (Isar); | file | diff | annotate |
2000-05-12 | paulson | updated | file | diff | annotate |
1998-11-16 | wenzelm | removed genelim.ML; | file | diff | annotate |
1998-10-20 | wenzelm | split_paired_all.ML: turn surjective pairing into split rule; | file | diff | annotate |
1998-02-26 | wenzelm | added clasimp.ML; | file | diff | annotate |
1998-02-12 | wenzelm | updated; | file | diff | annotate |
1997-11-26 | wenzelm | tuned; | file | diff | annotate |
1997-05-21 | wenzelm | tuned all READMEs; | file | diff | annotate |
1993-12-13 | lcp | added mention of simplifier, splitter, hypsubst | file | diff | annotate |
1993-09-16 | clasohm | Initial revision | file | diff | annotate |