src/HOL/Tools/Transfer/transfer.ML
2 months ago wenzelm 2019-06-04 misc tuning and clarification, notably wrt. flow of context;
4 months ago wenzelm 2019-04-13 tuned signature;
4 months ago wenzelm 2019-04-13 clarified: use existing Thm.dest_ctyp_fun (which is more strict);
7 months ago wenzelm 2019-01-05 isabelle update -u control_cartouches;
7 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
18 months ago wenzelm 2018-02-19 tuned signature;
19 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2016-10-31 kuncar 2016-10-31 always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-02-17 blanchet 2016-02-17 refactoring
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-10-09 kuncar 2015-10-09 new methods for debugging transfer and transfer_prover
2015-10-09 kuncar 2015-10-09 right parenthesization
2015-09-01 wenzelm 2015-09-01 tuned -- avoid slightly odd @{cpat};
2015-07-27 wenzelm 2015-07-27 tuned signature; clarified context;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
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-03 wenzelm 2015-06-03 clarified context;
2014-11-18 kuncar 2014-11-18 tuned; store pred_simps
2014-11-18 kuncar 2014-11-18 added pred_def, rel_eq_onp tuned
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-11 wenzelm 2015-02-11 proper context;
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-29 wenzelm 2014-10-29 modernized setup;
2014-04-25 wenzelm 2014-04-25 make SML/NJ happier;
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names