Thu, 13 Apr 2000 15:00:42 +0200 | wenzelm | intro/elim_tac: match only; | changeset | files |
Thu, 13 Apr 2000 10:30:28 +0200 | nipkow | made mod_less_divisor a simplification rule. | changeset | files |
Wed, 12 Apr 2000 23:52:50 +0200 | wenzelm | InductMethod.concls_of; | changeset | files |
Wed, 12 Apr 2000 23:52:21 +0200 | wenzelm | tuned; | changeset | files |
Wed, 12 Apr 2000 23:51:57 +0200 | wenzelm | export concl_of; | changeset | files |
Wed, 12 Apr 2000 23:49:10 +0200 | wenzelm | tuned \isasymlbrace; | changeset | files |
Wed, 12 Apr 2000 23:47:47 +0200 | wenzelm | 'insts' syntax; | changeset | files |
Wed, 12 Apr 2000 23:46:06 +0200 | wenzelm | improved 'induct(_tac)' syntax; | changeset | files |