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
Fri, 25 Jun 2010 15:16:22 +0200 remove junk
blanchet [Fri, 25 Jun 2010 15:16:22 +0200] rev 37568
remove junk
Fri, 25 Jun 2010 15:08:03 +0200 further reduce dependencies on "sledgehammer_fact_filter.ML"
blanchet [Fri, 25 Jun 2010 15:08:03 +0200] rev 37567
further reduce dependencies on "sledgehammer_fact_filter.ML"
Fri, 25 Jun 2010 15:01:35 +0200 move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
blanchet [Fri, 25 Jun 2010 15:01:35 +0200] rev 37566
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; since it has nothing to do with filtering
Mon, 28 Jun 2010 10:39:39 +0200 merged
wenzelm [Mon, 28 Jun 2010 10:39:39 +0200] rev 37565
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip