Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | fixes related to Refute's move | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | added a timeout around script that relies on the network | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | moved Refute to "HOL/Library" to speed up building "Main" even more | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | tuning | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | use metaquantification when possible in Isar proofs | changeset | files |
Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | tuned code | changeset | files |