| Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 23:07:01 +0200 |
krauss |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:36 +0100 |
blanchet |
rephrase some slow "metis" calls
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
more "metis" calls in example
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 06:01:47 +0100 |
huffman |
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 12:49:05 +0100 |
huffman |
Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
|
file |
diff |
annotate
|
| Thu, 27 Oct 2011 07:46:57 +0200 |
huffman |
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
file |
diff |
annotate
| base
|