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
blanchet [Wed, 23 Jun 2010 18:43:50 +0200] rev 37537
improve the new "natural formula" fact filter
wenzelm [Fri, 25 Jun 2010 11:48:37 +0200] rev 37536
explicit treatment of UTF8 sequences as Isabelle symbols;