| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make mangling sound w.r.t. type arguments
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make "filter_type_args" more robust if the actual arity is higher than the declared one
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
updated Sledgehammer documentation
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
changeset |
files
|
| Tue, 06 Sep 2011 22:41:35 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
changeset |
files
|
| Tue, 06 Sep 2011 16:30:39 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 14:53:51 -0700 |
huffman |
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
|
changeset |
files
|
| Wed, 07 Sep 2011 07:59:45 +0900 |
Cezary Kaliszyk |
HOL/Import: Update HOL4 generated files to current Isabelle.
|
changeset |
files
|
| Wed, 07 Sep 2011 00:08:09 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|