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
Wed, 31 Oct 2012 11:23:21 +0100 blanchet fixes related to Refute's move
Wed, 31 Oct 2012 11:23:21 +0100 blanchet added a timeout around script that relies on the network
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
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved Refute to "HOL/Library" to speed up building "Main" even more
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuning
Wed, 31 Oct 2012 11:23:21 +0100 blanchet use metaquantification when possible in Isar proofs
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuned code
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip