| Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
changeset |
files
|
| Thu, 26 Aug 2010 12:06:00 +0200 |
wenzelm |
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
|
changeset |
files
|
| Thu, 26 Aug 2010 11:33:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 26 Aug 2010 10:42:22 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 26 Aug 2010 10:42:06 +0200 |
blanchet |
consider "locality" when assigning weights to facts
|
changeset |
files
|
| Thu, 26 Aug 2010 09:23:21 +0200 |
blanchet |
add a bonus for chained facts, since they are likely to be relevant;
|
changeset |
files
|
| Thu, 26 Aug 2010 09:03:18 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 26 Aug 2010 01:03:08 +0200 |
blanchet |
add a penalty for lambda-abstractions;
|
changeset |
files
|
| Thu, 26 Aug 2010 00:49:38 +0200 |
blanchet |
renaming
|
changeset |
files
|
| Thu, 26 Aug 2010 00:49:04 +0200 |
blanchet |
fiddle with relevance filter
|
changeset |
files
|
| Wed, 25 Aug 2010 19:47:25 +0200 |
blanchet |
update docs
|
changeset |
files
|
| Wed, 25 Aug 2010 19:41:18 +0200 |
blanchet |
reorganize options regarding to the relevance threshold and decay
|
changeset |
files
|