Thu, 14 Apr 2011 11:24:05 +0200 nicer error message from Metis for know failure that isn't the user's fault
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42354
nicer error message from Metis for know failure that isn't the user's fault
Thu, 14 Apr 2011 11:24:05 +0200 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42353
correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
Thu, 14 Apr 2011 11:24:05 +0200 tuning
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42352
tuning
Thu, 14 Apr 2011 11:24:05 +0200 remove needless export
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42351
remove needless export
Thu, 14 Apr 2011 11:24:05 +0200 more clausification tests
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42350
more clausification tests
Thu, 14 Apr 2011 11:24:05 +0200 make 48170228f562 work also with "HO_Reas" examples
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42349
make 48170228f562 work also with "HO_Reas" examples
Thu, 14 Apr 2011 11:24:05 +0200 improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42348
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
Thu, 14 Apr 2011 11:24:05 +0200 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42347
properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
Thu, 14 Apr 2011 11:24:05 +0200 remove experimental code added in 85bb6fbb8e6a
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42346
remove experimental code added in 85bb6fbb8e6a
Thu, 14 Apr 2011 11:24:05 +0200 added examples of definitional CNF facts
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42345
added examples of definitional CNF facts
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip