2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
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-06 wenzelm 2015-03-06 tuned -- more explicit use of context;
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-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-28 wenzelm 2014-08-28 tuned;
2014-06-27 blanchet 2014-06-27 tuned whitespace and parentheses
2014-06-27 blanchet 2014-06-27 resolution modulo double negation
2014-06-16 fleury 2014-06-16 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-02-16 blanchet 2014-02-16 removed final periods in messages for proof methods
2014-02-01 wenzelm 2014-02-01 unused;
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate 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 simplified old code
2013-05-29 wenzelm 2013-05-29 resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-27 wenzelm 2013-05-27 instantiate types as well (see also Thm.first_order_match);
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-12 wenzelm 2013-05-12 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
2013-05-11 wenzelm 2013-05-11 avoid PolyML.makestring, even in dead code;
2013-04-12 wenzelm 2013-04-12 tuned exceptions -- avoid composing error messages in low-level situations;
2013-01-14 blanchet 2013-01-14 less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
2012-06-26 blanchet 2012-06-26 added type arguments to "ATerm" constructor -- but don't use them yet
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2012-02-02 blanchet 2012-02-02 implemented partial application aliases (for SPASS mainly)
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2011-11-18 blanchet 2011-11-18 wrap lambdas earlier, to get more control over beta/eta
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-08-25 blanchet 2011-08-25 avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-10 blanchet 2011-06-10 tuning
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09 wenzelm 2011-06-09 clarified special incr_type_indexes;
2011-06-09 blanchet 2011-06-09 removed needless function that duplicated standard functionality, with a little unnecessary twist
2011-06-09 blanchet 2011-06-09 removed more dead code
2011-06-09 blanchet 2011-06-09 renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
2011-06-08 wenzelm 2011-06-08 merged
2011-06-08 blanchet 2011-06-08 restore comment about subtle issue
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-06-08 blanchet 2011-06-08 removed yet another hack in "make_metis" script -- respect opacity of ""
2011-06-08 blanchet 2011-06-08 removed experimental code submitted by mistake
2011-06-08 blanchet 2011-06-08 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-07 blanchet 2011-06-07 nicely thread monomorphism verbosity in Metis and Sledgehammer
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 fall back in case path finder fails -- these errors are sometimes salvageable
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
2011-06-06 blanchet 2011-06-06 make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)