haftmann [Thu, 24 Jun 2010 21:04:35 +0200] rev 37542
more direct definition simplifies proofs
haftmann [Thu, 24 Jun 2010 21:03:32 +0200] rev 37541
merged
haftmann [Thu, 24 Jun 2010 18:45:31 +0200] rev 37540
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 37539
a76ace919f1c wasn't quite right; second try
blanchet [Thu, 24 Jun 2010 18:04:31 +0200] rev 37538
merge
blanchet [Thu, 24 Jun 2010 17:57:36 +0200] rev 37537
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 37536
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 37535
cosmetics
blanchet [Thu, 24 Jun 2010 10:38:01 +0200] rev 37534
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet [Wed, 23 Jun 2010 18:43:50 +0200] rev 37533
improve the new "natural formula" fact filter