src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
Wed, 22 May 2013 12:39:09 +0200 smolkas prevent pretty printer from automatically annotating numerals
Mon, 06 May 2013 11:03:08 +0200 smolkas avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
Mon, 18 Feb 2013 12:16:27 +0100 smolkas 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
Wed, 28 Nov 2012 12:25:43 +0100 smolkas added comments to new source files
Wed, 28 Nov 2012 12:22:17 +0100 smolkas put shrink in own structure
Wed, 28 Nov 2012 12:22:05 +0100 smolkas put annotate in own structure
less more (0) tip