| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
eta-contract to avoid needless "lambda" wrappers
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
quiet down SMT
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
more aggressive lambda hiding (if we anyway need to pass an option to Metis)
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
updated Sledgehammer docs
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't pass "lam_lifted" option to "metis" unless there's a good reason
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
no needless reconstructors
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed more clutter
|
changeset |
files
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed needless baggage
|
changeset |
files
|
| Fri, 18 Nov 2011 06:50:05 +0100 |
huffman |
Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs
|
changeset |
files
|
| Fri, 18 Nov 2011 04:56:35 +0100 |
huffman |
merged
|
changeset |
files
|
| Thu, 17 Nov 2011 18:31:00 +0100 |
huffman |
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
|
changeset |
files
|
| Thu, 17 Nov 2011 15:07:46 +0100 |
huffman |
HOL-Word: removed more duplicate theorems
|
changeset |
files
|