| Thu, 30 Nov 2000 20:05:34 +0100 |
wenzelm |
renamed "equivalence_class" to "class";
|
changeset |
files
|
| Thu, 30 Nov 2000 20:05:10 +0100 |
wenzelm |
schematic goals;
|
changeset |
files
|
| Thu, 30 Nov 2000 20:04:49 +0100 |
wenzelm |
cases/induct: tuned handling of facts ('consumes');
|
changeset |
files
|
| Thu, 30 Nov 2000 20:04:16 +0100 |
wenzelm |
'consumes' att;
|
changeset |
files
|
| Thu, 30 Nov 2000 20:03:39 +0100 |
wenzelm |
misc;
|
changeset |
files
|
| Thu, 30 Nov 2000 17:55:17 +0100 |
paulson |
replaced Eps by SOME
|
changeset |
files
|
| Thu, 30 Nov 2000 16:48:38 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 30 Nov 2000 14:10:23 +0100 |
bauerg |
some properties;
|
changeset |
files
|
| Thu, 30 Nov 2000 13:56:46 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 29 Nov 2000 18:42:40 +0100 |
wenzelm |
resolveq_cases_tac moved here from Pure/Isar/method.ML;
|
changeset |
files
|
| Wed, 29 Nov 2000 18:41:43 +0100 |
wenzelm |
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
|
changeset |
files
|
| Wed, 29 Nov 2000 17:24:20 +0100 |
nipkow |
expand_split_asm -> split_split_asm
|
changeset |
files
|
| Wed, 29 Nov 2000 17:23:27 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 29 Nov 2000 13:44:26 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 29 Nov 2000 10:22:38 +0100 |
paulson |
simproc for cancelling common factors around = < <= div /
|
changeset |
files
|