Thu, 30 Nov 2000 20:14:25 +0100 |
wenzelm |
removed "./configure";
|
changeset |
files
|
Thu, 30 Nov 2000 20:10:29 +0100 |
wenzelm |
/usr/bin/env bash;
|
changeset |
files
|
Thu, 30 Nov 2000 20:07:35 +0100 |
wenzelm |
schematic props;
|
changeset |
files
|
Thu, 30 Nov 2000 20:06:52 +0100 |
wenzelm |
removed get_goal;
|
changeset |
files
|
Thu, 30 Nov 2000 20:05:54 +0100 |
wenzelm |
added is_replaced_dummy_pattern;
|
changeset |
files
|
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
|
Wed, 29 Nov 2000 10:21:43 +0100 |
paulson |
invoking CancelNumeralFactorFun
|
changeset |
files
|
Wed, 29 Nov 2000 10:19:32 +0100 |
paulson |
new simproc file cancel_numeral_factor.ML
|
changeset |
files
|
Tue, 28 Nov 2000 16:21:51 +0100 |
paulson |
added a reference to {sec:products} for ordered pair reasoning
|
changeset |
files
|
Tue, 28 Nov 2000 01:48:07 +0100 |
wenzelm |
fixed hostname;
|
changeset |
files
|
Tue, 28 Nov 2000 01:23:45 +0100 |
wenzelm |
detect CVSROOT;
|
changeset |
files
|
Tue, 28 Nov 2000 01:22:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 28 Nov 2000 01:11:12 +0100 |
wenzelm |
added consumes, consumes_default;
|
changeset |
files
|
Tue, 28 Nov 2000 01:10:37 +0100 |
wenzelm |
resolveq_cases_tac: insert facts;
|
changeset |
files
|