src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
2013-11-19 ago tuning
2013-07-12 ago tuned
2013-07-09 ago moved code -> easier debugging
2013-06-26 ago ommit trivial tfrees in annotations
2013-06-11 ago uncheck terms before annotation to avoid awkward syntax
2013-06-11 ago make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
2013-05-22 ago prevent pretty printer from automatically annotating numerals
2013-05-06 ago avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
2013-02-18 ago split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
2012-11-28 ago added comments to new source files
2012-11-28 ago put shrink in own structure
2012-11-28 ago put annotate in own structure