| Mon, 23 Jun 2008 15:31:25 +0200 | wenzelm | induct_tac: mutual rules work as for method "induct"; | changeset | files |
| Mon, 23 Jun 2008 15:26:53 +0200 | wenzelm | tuned get_inductT: *all* rules for missing instantiation; | changeset | files |
| Mon, 23 Jun 2008 15:26:52 +0200 | wenzelm | induct_tac: infer mutual rule from types, as for proper induct method; | changeset | files |
| Mon, 23 Jun 2008 15:26:51 +0200 | wenzelm | induct_tac/case_tac: nested tuples are split as expected; | changeset | files |
| Mon, 23 Jun 2008 15:26:49 +0200 | wenzelm | induct_tac: old conjunctive rules no longer supported; | changeset | files |
| Mon, 23 Jun 2008 15:26:48 +0200 | wenzelm | updated generated file; | changeset | files |
| Mon, 23 Jun 2008 15:26:47 +0200 | wenzelm | induct_tac: rule is inferred from types; | changeset | files |