2011-03-31 boehmes [Thu, 31 Mar 2011 14:02:03 +0200] rev 42183
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
src/HOL/Tools/SMT/smt_monomorph.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2011-03-31 blanchet [Thu, 31 Mar 2011 11:16:54 +0200] rev 42182
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2011-03-31 blanchet [Thu, 31 Mar 2011 11:16:53 +0200] rev 42181
temporary workaround: filter out spurious monomorphic instances
src/HOL/Tools/SMT/smt_monomorph.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

2011-03-31 blanchet [Thu, 31 Mar 2011 11:16:52 +0200] rev 42180
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
NEWS doc-src/Sledgehammer/sledgehammer.tex src/HOL/Tools/SMT/smt_monomorph.ML src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

2011-03-31 blanchet [Thu, 31 Mar 2011 11:16:51 +0200] rev 42179
added support for "dest:" to "try"
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/try.ML

2011-03-31 haftmann [Thu, 31 Mar 2011 09:43:36 +0200] rev 42178
corrected infix precedence for boolean operators in Haskell
src/HOL/HOL.thy

2011-03-31 bulwahn [Thu, 31 Mar 2011 08:28:03 +0200] rev 42177
merged

2011-03-30 bulwahn [Wed, 30 Mar 2011 19:09:57 +0200] rev 42176
removing dead code in exhaustive_generators
src/HOL/Tools/Quickcheck/exhaustive_generators.ML

2011-03-30 bulwahn [Wed, 30 Mar 2011 19:09:56 +0200] rev 42175
removing junk that should not have been committed
src/HOL/Quickcheck.thy

2011-03-30 wenzelm [Wed, 30 Mar 2011 23:26:40 +0200] rev 42174
modernized specifications;
src/HOL/Hoare/Hoare_Logic.thy src/HOL/Hoare/Hoare_Logic_Abort.thy src/HOL/Hoare/SepLogHeap.thy src/HOL/Hoare_Parallel/Graph.thy src/HOL/Hoare_Parallel/OG_Com.thy src/HOL/Hoare_Parallel/OG_Tran.thy src/HOL/Hoare_Parallel/RG_Com.thy src/HOL/Hoare_Parallel/RG_Hoare.thy src/HOL/Hoare_Parallel/RG_Tran.thy src/HOL/IMP/Com.thy src/HOL/IMP/Denotation.thy src/HOL/IMP/Expr.thy src/HOL/IMP/Hoare.thy src/HOL/IMP/Machines.thy src/HOL/IMPP/Com.thy src/HOL/IMPP/Hoare.thy src/HOL/IOA/Asig.thy src/HOL/IOA/IOA.thy