| Wed, 24 Aug 2011 10:59:22 +0900 |
Cezary Kaliszyk |
Quotient Package: add mem_rsp, mem_prs, tune proofs.
|
changeset |
files
|
| Tue, 23 Aug 2011 15:46:53 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
changeset |
files
|
| Tue, 23 Aug 2011 07:12:05 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 18:15:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 16:49:45 -0700 |
huffman |
comment out dead code to avoid compiler warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 10:43:10 -0700 |
huffman |
legacy theorem names
|
changeset |
files
|
| Mon, 22 Aug 2011 10:19:39 -0700 |
huffman |
remove duplicate lemma
|
changeset |
files
|
| Tue, 23 Aug 2011 23:18:13 +0200 |
blanchet |
fixed "hBOOL" of existential variables, and generate more helpers
|
changeset |
files
|
| Tue, 23 Aug 2011 22:44:08 +0200 |
blanchet |
don't select facts when using sledgehammer_tac for reconstruction
|
changeset |
files
|
| Tue, 23 Aug 2011 20:35:41 +0200 |
blanchet |
don't perform a triviality check if the goal is skipped anyway
|
changeset |
files
|
| Tue, 23 Aug 2011 19:50:25 +0200 |
blanchet |
optional reconstructor
|
changeset |
files
|
| Wed, 24 Aug 2011 17:25:45 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|