Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | always minimize Sledgehammer results by default | changeset | files |
Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | tuned ML function name | changeset | files |
Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | reduced preplay timeout to 1 s | changeset | files |
Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | added more proof methods for one-liners | changeset | files |
Wed, 30 Jul 2014 23:52:56 +0200 | blanchet | unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings) | changeset | files |
Wed, 30 Jul 2014 14:03:58 +0200 | fleury | Improving robustness and indentation corrections. | changeset | files |