| Tue, 06 Sep 2011 08:00:28 -0700 |
huffman |
remove duplicate copy of lemma sqrt_add_le_add_sqrt
|
changeset |
files
|
| Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
changeset |
files
|
| Tue, 06 Sep 2011 07:45:18 -0700 |
huffman |
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
|
changeset |
files
|
| Tue, 06 Sep 2011 07:41:15 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 22:30:25 -0700 |
huffman |
add lemmas about arctan;
|
changeset |
files
|
| Mon, 05 Sep 2011 18:06:02 -0700 |
huffman |
convert lemma cos_total to Isar-style proof
|
changeset |
files
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
changeset |
files
|
| Tue, 06 Sep 2011 11:31:01 +0200 |
blanchet |
updated Sledgehammer's docs
|
changeset |
files
|
| Tue, 06 Sep 2011 11:31:01 +0200 |
blanchet |
cleanup "simple" type encodings
|
changeset |
files
|
| Tue, 06 Sep 2011 17:50:04 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Tue, 06 Sep 2011 16:45:31 +0900 |
Cezary Kaliszyk |
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
|
changeset |
files
|
| Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
drop more type arguments soundly, when they can be deduced from the arg types
|
changeset |
files
|
| Tue, 06 Sep 2011 20:55:18 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
changeset |
files
|
| Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
changeset |
files
|