| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
parse new experimental '@' encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:16 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 17:03:34 +0200 |
wenzelm |
clarified import;
|
changeset |
files
|
| Wed, 07 Sep 2011 16:53:49 +0200 |
wenzelm |
tuned/simplified proofs;
|
changeset |
files
|
| Wed, 07 Sep 2011 16:37:50 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:36:39 +0200 |
wenzelm |
deactivate unfinished charset provider for now, to avoid user confusion;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:26:27 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:17:19 +0200 |
wenzelm |
added "check" button: adhoc change to full buffer perspective;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:00:39 +0200 |
wenzelm |
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
|
changeset |
files
|
| 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
|
| Tue, 06 Sep 2011 13:16:46 -0700 |
huffman |
remove some unnecessary simp rules from simpset
|
changeset |
files
|
| Tue, 06 Sep 2011 21:56:11 +0200 |
wenzelm |
some Isabelle/jEdit NEWS;
|
changeset |
files
|
| Tue, 06 Sep 2011 21:40:58 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Tue, 06 Sep 2011 21:11:12 +0200 |
wenzelm |
merged
|
changeset |
files
|