Fri, 25 Jun 2010 17:08:39 +0200 renamed "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 +0200 merge "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 +0200 get 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 +0200 exploit "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 +0200 renamed "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 +0200 fewer dependencies
blanchet [Fri, 25 Jun 2010 16:03:34 +0200] rev 37573
fewer dependencies
Fri, 25 Jun 2010 15:59:13 +0200 more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet [Fri, 25 Jun 2010 15:59:13 +0200] rev 37572
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
Fri, 25 Jun 2010 15:30:38 +0200 more moving around of ML files in "Sledgehammer.thy"
blanchet [Fri, 25 Jun 2010 15:30:38 +0200] rev 37571
more moving around of ML files in "Sledgehammer.thy"
Fri, 25 Jun 2010 15:22:12 +0200 got rid of needless exception
blanchet [Fri, 25 Jun 2010 15:22:12 +0200] rev 37570
got rid of needless exception
Fri, 25 Jun 2010 15:18:58 +0200 move "MESON" up;
blanchet [Fri, 25 Jun 2010 15:18:58 +0200] rev 37569
move "MESON" up; the ultimate goal is to make Sledgehammer depend on MESON and Metis, rather than a big spaghetti
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip