src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
2012-04-24 sultana 2012-04-24 reversed Tools to Actions Mirabelle renaming;
2012-03-30 sultana 2012-03-30 made Mirabelle-SH's 'trivial' check optional;
2012-03-27 blanchet 2012-03-27 more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-20 blanchet 2012-03-20 added term_order option to Mirabelle
2012-03-20 blanchet 2012-03-20 more weight attribute tuning
2012-03-20 blanchet 2012-03-20 internal renamings
2012-03-07 sultana 2012-03-07 added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
2012-03-07 sultana 2012-03-07 added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-05 blanchet 2012-02-05 tuning
2012-02-04 blanchet 2012-02-04 added option to Mirabelle/Sledgehammer
2012-01-31 blanchet 2012-01-31 renamed Sledgehammer option
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-26 blanchet 2012-01-26 separate orthogonal components
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2011-12-01 blanchet 2011-12-01 renamed "slicing" to "slice"
2011-11-16 blanchet 2011-11-16 thread in additional options to minimizer
2011-11-16 blanchet 2011-11-16 make metis reconstruction handling more flexible
2011-11-16 blanchet 2011-11-16 parse lambda translation option in Metis
2011-11-15 blanchet 2011-11-15 rename configuration option to more reasonable length
2011-11-06 blanchet 2011-11-06 tuning
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-02 blanchet 2011-09-02 renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-09-01 blanchet 2011-09-01 always measure time for ATPs -- auto minimization relies on it
2011-09-01 blanchet 2011-09-01 make "sound" sound and "unsound" more sound, based on evaluation
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-30 blanchet 2011-08-30 extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-08-28 blanchet 2011-08-28 split timeout among ATPs in and add Metis to the mix as backup
2011-08-27 blanchet 2011-08-27 beef up sledgehammer_tac in Mirabelle some more
2011-08-25 blanchet 2011-08-25 include chained facts for minimizer, otherwise it won't work
2011-08-24 blanchet 2011-08-24 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-24 blanchet 2011-08-24 specify timeout for "sledgehammer_tac"
2011-08-23 blanchet 2011-08-23 don't select facts when using sledgehammer_tac for reconstruction
2011-08-23 blanchet 2011-08-23 don't perform a triviality check if the goal is skipped anyway
2011-08-23 blanchet 2011-08-23 optional reconstructor
2011-08-23 blanchet 2011-08-23 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
2011-08-23 blanchet 2011-08-23 beef up "sledgehammer_tac" reconstructor
2011-08-23 blanchet 2011-08-23 clearer separator in generated file names
2011-08-09 blanchet 2011-08-09 support local HOATPs
2011-08-09 blanchet 2011-08-09 add line number prefix to output file name
2011-08-09 blanchet 2011-08-09 added "sound" option to Mirabelle
2011-07-20 blanchet 2011-07-20 remove offset from Mirabelle output
2011-07-14 blanchet 2011-07-14 move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
2011-07-14 blanchet 2011-07-14 added option to control which lambda translation to use (for experiments)
2011-07-08 wenzelm 2011-07-08 discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate
2011-06-27 blanchet 2011-06-27 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-10 blanchet 2011-06-10 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-08 blanchet 2011-06-08 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 enable new Metis
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 show what failed to play
2011-05-31 blanchet 2011-05-31 compile
2011-05-30 blanchet 2011-05-30 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30 blanchet 2011-05-30 automatically minimize with Metis when this can be done within a few seconds