| Thu, 04 Oct 2001 16:09:12 +0200 | wenzelm | induct/cases made generic, removed simplified/stripped options; | changeset | files |
| Thu, 04 Oct 2001 16:07:43 +0200 | wenzelm | improved proof by cases and induction; | changeset | files |
| Thu, 04 Oct 2001 16:07:20 +0200 | wenzelm | removed obsolete comment; | changeset | files |
| Thu, 04 Oct 2001 15:43:17 +0200 | wenzelm | generic induct_method.ML; | changeset | files |
| Thu, 04 Oct 2001 15:42:48 +0200 | wenzelm | non-oriented infix = and ~= (output only); | changeset | files |
| Thu, 04 Oct 2001 15:41:43 +0200 | wenzelm | $(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML; | changeset | files |
| Thu, 04 Oct 2001 15:40:52 +0200 | wenzelm | use "~~/src/Provers/induct_method.ML"; | changeset | files |
| Thu, 04 Oct 2001 15:40:31 +0200 | wenzelm | removed hol_rewrite_cterm (use full_rewrite_cterm from Pure); | changeset | files |