Fri, 30 Dec 2011 17:45:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
Fri, 30 Dec 2011 11:11:57 +0100 |
huffman |
remove unnecessary intermediate lemmas
|
changeset |
files
|
Fri, 30 Dec 2011 17:40:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 30 Dec 2011 16:43:46 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms;
|
changeset |
files
|
Fri, 30 Dec 2011 15:43:07 +0100 |
wenzelm |
simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;
|
changeset |
files
|
Fri, 30 Dec 2011 14:19:58 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
Fri, 30 Dec 2011 13:52:07 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
Fri, 30 Dec 2011 12:54:55 +0100 |
wenzelm |
simplified proof;
|
changeset |
files
|
Fri, 30 Dec 2011 12:12:16 +0100 |
wenzelm |
more parallelism;
|
changeset |
files
|
Fri, 30 Dec 2011 12:00:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 29 Dec 2011 20:32:59 +0100 |
wenzelm |
merged
|
changeset |
files
|
Thu, 29 Dec 2011 20:31:58 +0100 |
wenzelm |
tuned -- afford slightly larger simpset in simp_defs_tac;
|
changeset |
files
|
Thu, 29 Dec 2011 20:05:53 +0100 |
wenzelm |
tuned -- standard proofs by default;
|
changeset |
files
|
Thu, 29 Dec 2011 19:37:24 +0100 |
wenzelm |
do not fork skipped proofs;
|
changeset |
files
|