src/HOL/Tools/Metis/metis_tactic.ML
2015-06-02 wenzelm 2015-06-02 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-30 wenzelm 2014-10-30 proper syntax categery "name" -- as usual and as documented;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-06-27 blanchet 2014-06-27 tuned whitespace and parentheses
2014-06-16 blanchet 2014-06-16 simplified code
2014-02-16 blanchet 2014-02-16 removed final periods in messages for proof methods
2014-02-16 blanchet 2014-02-16 added a version of the Metis tactic that returns the unused facts
2014-02-16 blanchet 2014-02-16 tuned code
2014-02-04 blanchet 2014-02-04 removed legacy 'metisFT' method
2014-02-03 blanchet 2014-02-03 merged 'reconstructors' and 'proof methods'
2014-02-02 blanchet 2014-02-02 rationalized threading of 'metis' arguments
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2014-01-02 blanchet 2014-01-02 removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-15 blanchet 2013-12-15 tuning
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-19 blanchet 2013-11-19 refactoring
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-01-14 blanchet 2013-01-14 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2013-01-03 blanchet 2013-01-03 avoid repeated calls to metis from "resolve_tac" in case of ultimate failure
2012-03-20 blanchet 2012-03-20 more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")
2012-03-20 blanchet 2012-03-20 enable "metis_advisory_simp" by default
2012-03-20 blanchet 2012-03-20 added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
2012-03-19 blanchet 2012-03-19 better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2012-01-19 blanchet 2012-01-19 renamed "sound" option to "strict"
2011-12-14 blanchet 2011-12-14 killed dead code
2011-11-18 blanchet 2011-11-18 more robust options
2011-11-18 blanchet 2011-11-18 pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
2011-11-18 blanchet 2011-11-18 wrap lambdas earlier, to get more control over beta/eta
2011-11-18 blanchet 2011-11-18 move eta-contraction to before translation to Metis, to ensure everything stays in sync
2011-11-18 blanchet 2011-11-18 avoid that var names get changed by resolution in Metis lambda-lifting
2011-11-18 blanchet 2011-11-18 avoid spurious messages in "lam_lifting" mode
2011-11-18 blanchet 2011-11-18 eta-contract to avoid needless "lambda" wrappers
2011-11-16 blanchet 2011-11-16 give each time slice its own lambda translation
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 the lambda translation schemes, so that they are understandable out of context
2011-11-15 blanchet 2011-11-15 rename configuration option to more reasonable length
2011-11-15 blanchet 2011-11-15 continued implementation of lambda-lifting in Metis
2011-11-15 blanchet 2011-11-15 started implementing lambda-lifting in Metis
2011-09-22 blanchet 2011-09-22 better type reconstruction -- prevents ill-instantiations in proof replay
2011-09-15 blanchet 2011-09-15 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)