| Wed, 30 Jul 2014 14:03:11 +0200 | fleury | Skolemization support for leo-II and Zipperposition. | changeset | files |
| Wed, 30 Jul 2014 10:50:30 +0200 | desharna | document property 'set_induct' | changeset | files |
| Wed, 30 Jul 2014 10:50:28 +0200 | desharna | generate 'set_induct' theorem for codatatypes | changeset | files |
| Wed, 30 Jul 2014 00:50:41 +0200 | blanchet | also try 'metis' with 'full_types' | changeset | files |
| Tue, 29 Jul 2014 23:39:35 +0200 | blanchet | header tuning | changeset | files |
| Mon, 28 Jul 2014 10:57:33 +0200 | blanchet | correctly translate THF functions from terms to types | changeset | files |
| Sun, 27 Jul 2014 21:11:35 +0200 | blanchet | do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly | changeset | files |
| Sun, 27 Jul 2014 15:44:08 +0200 | wenzelm | back to post-release mode -- after fork point; | changeset | files |