Thu, 25 Nov 2010 13:26:12 +0100 blanchet set Metis option on correct context, lest it be ignored
Thu, 25 Nov 2010 12:11:12 +0100 blanchet make "debug" mode of Sledgehammer/SMT more liberal
Thu, 25 Nov 2010 00:32:30 +0100 blanchet fix check for builtinness of 0 and 1 -- these aren't functions
Thu, 25 Nov 2010 00:17:16 +0100 blanchet added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
Wed, 24 Nov 2010 23:17:24 +0100 blanchet document requirement on theory import
Wed, 24 Nov 2010 19:15:00 +0100 haftmann corrected abd4e7358847 where SOMEthing went utterly wrong
Wed, 24 Nov 2010 16:51:13 +0100 boehmes merged
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip