src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
2013-11-19 ago tuning
2013-11-19 ago tuning
2013-09-20 ago hardcoded obscure option
2013-09-20 ago hard-coded an obscure option
2013-07-17 ago tuned
2013-07-13 ago tuned
2013-07-12 ago cleaner preplay interface
2013-07-12 ago preplay failures might be resolved later, so proceed as usual
2013-07-11 ago optimize isar-proofs by trying different proof methods
2013-07-11 ago made SML/NJ happy
2013-07-09 ago completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-06-26 ago tuned: cleaned up data structure
2013-06-26 ago simplified data structure
2013-05-17 ago tuned signature;
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-11 ago never open structure Unsynchronized (cf. "implementation" manual);
2013-05-11 ago prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-05-06 ago added preplay tracing
2013-05-06 ago avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
2013-05-06 ago added informative error messages
2013-04-23 ago tuning
2013-02-24 ago tuned agressiveness of isar compression
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
2013-02-18 ago simplified byline, isar_qualifier
2013-02-15 ago removed dead weight from data structure
2013-02-14 ago renamed sledgehammer_shrink to sledgehammer_compress