Thu, 24 Apr 1997 19:41:00 +0200 | wenzelm | adapted to SML/NJ 1.09.27; | changeset | files |
Thu, 24 Apr 1997 19:08:32 +0200 | nipkow | Added 'induct_tac' | changeset | files |
Thu, 24 Apr 1997 18:51:14 +0200 | nipkow | Updates because nat_ind_tac no longer appends "1" to the ind.var. | changeset | files |
Thu, 24 Apr 1997 18:44:32 +0200 | wenzelm | removed space; | changeset | files |
Thu, 24 Apr 1997 18:38:30 +0200 | nipkow | induct_tac | changeset | files |
Thu, 24 Apr 1997 18:07:35 +0200 | mueller | expandshort | changeset | files |
Thu, 24 Apr 1997 18:06:46 +0200 | nipkow | Introduced a generic "induct_tac" which picks up the right induction scheme | changeset | files |
Thu, 24 Apr 1997 18:03:23 +0200 | nipkow | get_thydata accesses the second component of the data field. This component | changeset | files |