| Tue, 17 Jun 2014 16:02:49 +0200 |
blanchet |
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
|
changeset |
files
|
| Mon, 16 Jun 2014 19:44:02 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 16 Jun 2014 19:42:44 +0200 |
blanchet |
integrated new Waldmeister code with 'sledgehammer' command
|
changeset |
files
|
| Mon, 16 Jun 2014 19:41:42 +0200 |
blanchet |
fixed parsing of one-argument 'file()' in TSTP files
|
changeset |
files
|
| Mon, 16 Jun 2014 19:41:01 +0200 |
blanchet |
use right delimiters for Waldmeister proofs
|
changeset |
files
|
| Mon, 16 Jun 2014 19:41:00 +0200 |
blanchet |
added 'waldmeister_new' as ATP
|
changeset |
files
|
| Mon, 16 Jun 2014 19:40:59 +0200 |
blanchet |
simplified code
|
changeset |
files
|
| Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
changeset |
files
|
| Mon, 16 Jun 2014 19:39:41 +0200 |
blanchet |
give Z3 TPTP proofs a chance
|
changeset |
files
|
| Mon, 16 Jun 2014 19:18:10 +0200 |
blanchet |
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
|
changeset |
files
|
| Mon, 16 Jun 2014 17:52:33 +0200 |
hoelzl |
add more derivative and continuity rules for complex-values functions
|
changeset |
files
|
| Mon, 16 Jun 2014 16:21:52 +0200 |
fleury |
Moving the remote prefix deleting on Sledgehammer's side
|
changeset |
files
|
| Mon, 16 Jun 2014 16:21:39 +0200 |
fleury |
Correcting the type parser
|
changeset |
files
|
| Mon, 16 Jun 2014 16:18:34 +0200 |
fleury |
imported patch leo2_skolem_simplication
|
changeset |
files
|
| Mon, 16 Jun 2014 16:18:15 +0200 |
fleury |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
changeset |
files
|
| Mon, 16 Jun 2014 13:19:48 +0200 |
hoelzl |
lemmas about the moments of the normal distribution
|
changeset |
files
|