| Thu, 29 Jun 2000 12:15:08 +0200 |
paulson |
fixed proof to cope with the default of equalityCE instead of equalityE
|
changeset |
files
|
| Thu, 29 Jun 2000 12:14:45 +0200 |
paulson |
now uses equalityCE, which usually is more efficent than equalityE
|
changeset |
files
|
| Thu, 29 Jun 2000 12:14:04 +0200 |
paulson |
weak elimination rules
|
changeset |
files
|
| Wed, 28 Jun 2000 21:15:02 +0200 |
wenzelm |
classical 'elimify' attribute;
|
changeset |
files
|
| Wed, 28 Jun 2000 19:57:16 +0200 |
kleing |
tuned for ProofGeneral 3.2
|
changeset |
files
|
| Wed, 28 Jun 2000 19:56:21 +0200 |
kleing |
tuning, eliminated rev_surj
|
changeset |
files
|
| Wed, 28 Jun 2000 12:39:30 +0200 |
paulson |
fixed some weak elim rules, and tidied
|
changeset |
files
|
| Wed, 28 Jun 2000 12:34:08 +0200 |
paulson |
tidying and unbatchifying
|
changeset |
files
|
| Wed, 28 Jun 2000 12:16:36 +0200 |
paulson |
no longer depends upon a prior "open Ind_Syntax" from elsewhere
|
changeset |
files
|
| Wed, 28 Jun 2000 12:15:56 +0200 |
paulson |
fixed some weak elim rules, and tidied
|
changeset |
files
|
| Wed, 28 Jun 2000 12:15:28 +0200 |
paulson |
fixed some weak elim rules
|
changeset |
files
|
| Wed, 28 Jun 2000 11:00:13 +0200 |
paulson |
simplified slightly by using dependencies better in theories
|
changeset |
files
|
| Wed, 28 Jun 2000 10:58:06 +0200 |
paulson |
finally theory Bin (the integers) is included
|
changeset |
files
|
| Wed, 28 Jun 2000 10:57:35 +0200 |
paulson |
FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG
|
changeset |
files
|
| Wed, 28 Jun 2000 10:56:34 +0200 |
paulson |
fixed some weak elim rules
|
changeset |
files
|
| Wed, 28 Jun 2000 10:56:01 +0200 |
paulson |
implements a classical version of make_elim
|
changeset |
files
|