| Wed, 09 Oct 2013 09:53:18 +0200 |
blanchet |
use plain types instead of dedicated type pattern
|
changeset |
files
|
| Wed, 09 Oct 2013 09:51:24 +0200 |
blanchet |
duplicate term and type patterns
|
changeset |
files
|
| Wed, 09 Oct 2013 09:47:59 +0200 |
blanchet |
optimized built-in const check
|
changeset |
files
|
| Wed, 09 Oct 2013 08:28:36 +0200 |
blanchet |
added TODO
|
changeset |
files
|
| Wed, 09 Oct 2013 08:12:53 +0200 |
blanchet |
crank up limit a bit -- truly huge background theories are still nearly 3 times larger
|
changeset |
files
|
| Tue, 08 Oct 2013 22:33:05 +0200 |
blanchet |
higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
|
changeset |
files
|
| Tue, 08 Oct 2013 21:19:46 +0200 |
blanchet |
minor fact filter speedups
|
changeset |
files
|
| Tue, 08 Oct 2013 20:56:35 +0200 |
blanchet |
more gracefully handle huge theories in relevance filters
|
changeset |
files
|
| Tue, 08 Oct 2013 20:53:37 +0200 |
blanchet |
handle huge MaSh requests gracefully
|
changeset |
files
|
| Tue, 08 Oct 2013 16:40:03 +0200 |
blanchet |
further optimization in relevance filter
|
changeset |
files
|
| Tue, 08 Oct 2013 14:53:33 +0200 |
blanchet |
further speed up duplicate elimination
|
changeset |
files
|
| Tue, 08 Oct 2013 14:41:25 +0200 |
blanchet |
more efficient theorem variable normalization
|
changeset |
files
|
| Mon, 07 Oct 2013 23:44:53 +0200 |
blanchet |
strengthened constructor-view tactic to deal with 'let's
|
changeset |
files
|
| Mon, 07 Oct 2013 23:38:57 +0200 |
blanchet |
allow 'let's around constructors in constructor view
|
changeset |
files
|