2010-06-25 blanchet [Fri, 25 Jun 2010 15:30:38 +0200] rev 37571
more moving around of ML files in "Sledgehammer.thy"
src/HOL/Sledgehammer.thy src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML

2010-06-25 blanchet [Fri, 25 Jun 2010 15:22:12 +0200] rev 37570
got rid of needless exception
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML

2010-06-25 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
src/HOL/Sledgehammer.thy

2010-06-25 blanchet [Fri, 25 Jun 2010 15:16:22 +0200] rev 37568
remove junk
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML

2010-06-25 blanchet [Fri, 25 Jun 2010 15:08:03 +0200] rev 37567
further reduce dependencies on "sledgehammer_fact_filter.ML"
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2010-06-25 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
src/HOL/Tools/Sledgehammer/metis_tactics.ML src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML

2010-06-28 wenzelm [Mon, 28 Jun 2010 10:39:39 +0200] rev 37565
merged

2010-06-28 Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Jun 2010 09:48:36 +0200] rev 37564
Quotient package reverse lifting
src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/Quotient/quotient_term.ML

2010-06-28 Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Jun 2010 07:38:39 +0200] rev 37563
Add reverse lifting flag to automated theorem derivation
src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/Quotient/quotient_term.ML

2010-06-28 Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Jun 2010 07:32:51 +0200] rev 37562
Restrict quotient definitions to constants
src/HOL/Tools/Quotient/quotient_def.ML