| Mon, 12 Nov 2001 10:44:55 +0100 |
berghofe |
congc now returns None if congruence rule has no effect.
|
changeset |
files
|
| Mon, 12 Nov 2001 10:43:25 +0100 |
berghofe |
Renamed some bound variables due to changes in simplifier.
|
changeset |
files
|
| Mon, 12 Nov 2001 10:39:42 +0100 |
berghofe |
Fixed proof depending on strange behaviour of rename_bvs.
|
changeset |
files
|
| Mon, 12 Nov 2001 10:37:36 +0100 |
berghofe |
Renamed some bound variables due to changes in simplifier.
|
changeset |
files
|
| Sun, 11 Nov 2001 21:38:54 +0100 |
wenzelm |
present multi_result;
|
changeset |
files
|
| Sun, 11 Nov 2001 21:38:25 +0100 |
wenzelm |
added meta_conjunction_tr';
|
changeset |
files
|
| Sun, 11 Nov 2001 21:38:04 +0100 |
wenzelm |
pure_syntax_output: "_meta_conjunction";
|
changeset |
files
|
| Sun, 11 Nov 2001 21:37:44 +0100 |
wenzelm |
adapted to multiple results;
|
changeset |
files
|
| Sun, 11 Nov 2001 21:37:20 +0100 |
wenzelm |
adapted auto_bind_goal, auto_bind_facts;
|
changeset |
files
|
| Sun, 11 Nov 2001 21:36:40 +0100 |
wenzelm |
added multi_theorem(_i);
|
changeset |
files
|
| Sun, 11 Nov 2001 21:35:21 +0100 |
wenzelm |
Proof.have_i: multiple statements;
|
changeset |
files
|
| Sun, 11 Nov 2001 21:35:04 +0100 |
wenzelm |
added RAW_METHOD, RAW_METHOD_CASES;
|
changeset |
files
|