| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 17:23:16 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 16:34:26 +0200 |
blanchet |
handle relevance filter corner cases more gracefully;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 18:22:04 +0200 |
blanchet |
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 16:32:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:50:51 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 17:27:10 +0200 |
blanchet |
got rid of the "theory_relevant" option;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 16:46:11 +0200 |
blanchet |
generalize theorem argument parsing syntax
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 11:59:04 +0200 |
blanchet |
fiddled with fudge factor (based on Mirabelle)
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 11:36:02 +0200 |
blanchet |
give priority to assumptions in structured proofs
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 10:26:54 +0200 |
blanchet |
introduce fudge factors to deal with "theory const"
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:50:59 +0200 |
blanchet |
finished renaming
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 23:46:23 +0200 |
blanchet |
shorten a few file names
|
file |
diff |
annotate
| base
|