Fri, 25 Jun 2010 18:03:01 +0200update docs
blanchet [Fri, 25 Jun 2010 18:03:01 +0200] rev 37582
update docs

Fri, 25 Jun 2010 17:32:55 +0200simpler argument
blanchet [Fri, 25 Jun 2010 17:32:55 +0200] rev 37581
simpler argument

Fri, 25 Jun 2010 17:26:14 +0200got rid of "respect_no_atp" option, which even I don't use
blanchet [Fri, 25 Jun 2010 17:26:14 +0200] rev 37580
got rid of "respect_no_atp" option, which even I don't use

Fri, 25 Jun 2010 17:13:38 +0200reorder ML files
blanchet [Fri, 25 Jun 2010 17:13:38 +0200] rev 37579
reorder ML files

Fri, 25 Jun 2010 17:08:39 +0200renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet [Fri, 25 Jun 2010 17:08:39 +0200] rev 37578
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer

Fri, 25 Jun 2010 16:42:06 +0200merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet [Fri, 25 Jun 2010 16:42:06 +0200] rev 37577
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME

Fri, 25 Jun 2010 16:29:07 +0200get rid of type alias
blanchet [Fri, 25 Jun 2010 16:29:07 +0200] rev 37576
get rid of type alias

Fri, 25 Jun 2010 16:27:53 +0200exploit "Name.desymbolize" to remove some dependencies
blanchet [Fri, 25 Jun 2010 16:27:53 +0200] rev 37575
exploit "Name.desymbolize" to remove some dependencies

Fri, 25 Jun 2010 16:15:03 +0200renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet [Fri, 25 Jun 2010 16:15:03 +0200] rev 37574
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)

Fri, 25 Jun 2010 16:03:34 +0200fewer dependencies
blanchet [Fri, 25 Jun 2010 16:03:34 +0200] rev 37573
fewer dependencies