2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44404
tuning, plus started implementing tag equation generation for existential variables
src/HOL/Tools/ATP/atp_translate.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44403
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
src/HOL/Tools/ATP/atp_translate.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44402
clearer terminology
src/HOL/Metis_Examples/Type_Encodings.thy src/HOL/TPTP/ATP_Export.thy src/HOL/Tools/ATP/atp_problem.ML src/HOL/Tools/ATP/atp_translate.ML src/HOL/Tools/Metis/metis_tactics.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44401
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
doc-src/Sledgehammer/sledgehammer.tex

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44400
removed unused configuration option
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44399
added caching for (in)finiteness checks
src/HOL/Tools/ATP/atp_reconstruct.ML src/HOL/Tools/ATP/atp_translate.ML src/HOL/Tools/ATP/atp_util.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44398
remove needless typing information
src/HOL/Tools/ATP/atp_translate.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44397
cleaner handling of polymorphic monotonicity inference
src/HOL/TPTP/atp_export.ML src/HOL/Tools/ATP/atp_translate.ML src/HOL/Tools/Metis/metis_translate.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44396
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
src/HOL/Tools/ATP/atp_reconstruct.ML src/HOL/Tools/ATP/atp_translate.ML src/HOL/Tools/Metis/metis_translate.ML

2011-08-22 blanchet [Mon, 22 Aug 2011 15:02:45 +0200] rev 44395
more precise warning
src/HOL/Tools/Nitpick/nitpick.ML