src/HOL/Tools/Lifting/lifting_def.ML
2015-05-03 wenzelm 2015-05-03 make SML/NJ more happy;
2015-05-02 kuncar 2015-05-02 don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
2015-04-13 kuncar 2015-04-13 go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
2014-12-05 kuncar 2014-12-05 Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
2014-12-05 kuncar 2014-12-05 return also which code equation was used; tuned
2014-12-05 kuncar 2014-12-05 note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
2014-11-18 kuncar 2014-11-18 export the result of lifting_def
2014-11-18 kuncar 2014-11-18 improve handling of predicators in rsp_thm
2014-11-18 kuncar 2014-11-18 lift_definition: return the result of lifting
2014-11-18 kuncar 2014-11-18 lift_definition: interface also with tactic
2014-11-18 kuncar 2014-11-18 generalize prove_schematic_quot_thm
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
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-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-28 haftmann 2015-01-28 abstract code equation may also be default
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-07-24 kuncar 2014-07-24 having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
2014-07-24 kuncar 2014-07-24 store explicitly quotient types with no_code => more precise registration of code equations
2014-07-24 kuncar 2014-07-24 prevent beta-contraction in proving extra assumptions for abs_eq
2014-04-11 kuncar 2014-04-11 fix the reflexivity prover
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 more appropriate name (Lifting.invariant -> eq_onp)
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-27 kuncar 2014-02-27 hide Lifting.invariant from a user completely
2014-02-25 kuncar 2014-02-25 new rule for making rsp theorem more readable
2014-02-25 kuncar 2014-02-25 the rules are not needed due to 1726f46d2aa8
2014-02-25 kuncar 2014-02-25 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
2014-02-24 kuncar 2014-02-24 more robust registration of code equations
2014-02-24 kuncar 2014-02-24 be consistent and produce always rep_eq with =
2014-02-20 kuncar 2014-02-20 refactoring; generate rep_eq always, not only when it would be accepted by the code generator
2014-02-20 kuncar 2014-02-20 refactoring
2014-02-20 kuncar 2014-02-20 the rule is not needed due to 1726f46d2aa8
2014-02-18 kuncar 2014-02-18 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
2014-01-11 wenzelm 2014-01-11 more accurate context;
2014-01-08 kuncar 2014-01-08 typo
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-10-14 kuncar 2013-10-14 update documentation of important public ML functions in Lifting
2013-09-27 kuncar 2013-09-27 allow to specify multiple parametricity transfer rules in lift_definition
2013-09-16 kuncar 2013-09-16 restoring Transfer/Lifting context
2013-08-26 wenzelm 2013-08-26 prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;
2013-08-26 wenzelm 2013-08-26 proper context;
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-05-13 kuncar 2013-05-13 typo
2013-05-10 kuncar 2013-05-10 don't apply an unnecessary morphism
2013-03-08 kuncar 2013-03-08 lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2012-10-24 huffman 2012-10-24 transfer package: more flexible handling of equality relations using is_equality predicate
2012-10-17 kuncar 2012-10-17 don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
2012-09-27 kuncar 2012-09-27 mk_readable_rsp_thm_eq is more robust now
2012-09-27 kuncar 2012-09-27 new get function for non-symmetric relator_eq & tuned
2012-05-29 kuncar 2012-05-29 don't be so aggressive during unfolding id and o