src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
Mon, 06 May 2013 11:03:08 +0200 smolkas added preplay tracing
Mon, 06 May 2013 11:03:08 +0200 smolkas avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
Mon, 06 May 2013 11:03:08 +0200 smolkas added informative error messages
Tue, 23 Apr 2013 16:30:30 +0200 blanchet tuning
Sun, 24 Feb 2013 15:49:07 +0100 smolkas tuned agressiveness of isar compression
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
Mon, 18 Feb 2013 12:16:02 +0100 smolkas simplified byline, isar_qualifier
Fri, 15 Feb 2013 10:18:44 +0100 blanchet removed dead weight from data structure
Thu, 14 Feb 2013 22:49:22 +0100 smolkas renamed sledgehammer_shrink to sledgehammer_compress
less more (0) tip