haftmann [Fri, 25 Jun 2010 07:19:21 +0200] rev 37547
merged
haftmann [Thu, 24 Jun 2010 21:04:35 +0200] rev 37546
more direct definition simplifies proofs
haftmann [Thu, 24 Jun 2010 21:03:32 +0200] rev 37545
merged
haftmann [Thu, 24 Jun 2010 18:45:31 +0200] rev 37544
more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)
blanchet [Thu, 24 Jun 2010 18:22:15 +0200] rev 37543
a76ace919f1c wasn't quite right; second try
blanchet [Thu, 24 Jun 2010 18:04:31 +0200] rev 37542
merge
blanchet [Thu, 24 Jun 2010 17:57:36 +0200] rev 37541
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
blanchet [Thu, 24 Jun 2010 17:27:18 +0200] rev 37540
better eta-expansion in Sledgehammer's clausification;
make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things
blanchet [Thu, 24 Jun 2010 17:25:47 +0200] rev 37539
cosmetics
blanchet [Thu, 24 Jun 2010 10:38:01 +0200] rev 37538
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds