| Fri, 03 Nov 2000 21:33:15 +0100 | wenzelm | provide case names for rev_induct, rev_cases; | changeset | files |
| Fri, 03 Nov 2000 21:32:41 +0100 | wenzelm | rev_exhaust: rulify; | changeset | files |
| Fri, 03 Nov 2000 21:31:53 +0100 | wenzelm | removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML); | changeset | files |
| Fri, 03 Nov 2000 21:31:11 +0100 | wenzelm | "atomize" for classical tactics; | changeset | files |
| Fri, 03 Nov 2000 21:29:56 +0100 | wenzelm | atomize: all automated tactics that "solve" goals; | changeset | files |
| Fri, 03 Nov 2000 21:28:15 +0100 | wenzelm | fixed two obscurities of "fix": predeclare_terms; | changeset | files |
| Fri, 03 Nov 2000 21:27:36 +0100 | wenzelm | tuned names; | changeset | files |
| Fri, 03 Nov 2000 21:27:06 +0100 | wenzelm | improved handling of "that": insert into goal, only declare as Pure "intro"; | changeset | files |