src/HOL/Tools/Lifting/lifting_def.ML
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
2012-05-24 kuncar 2012-05-24 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
2012-05-21 kuncar 2012-05-21 quot_del attribute, it allows us to deregister quotient types
2012-05-16 kuncar 2012-05-16 generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-05-02 kuncar 2012-05-02 documentation of the Lifting package on the ML level & tuned
2012-04-23 kuncar 2012-04-23 added useful Trueprop_conv
2012-04-23 kuncar 2012-04-23 move MRSL to a separate file
2012-04-22 huffman 2012-04-22 fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
2012-04-20 kuncar 2012-04-20 hide the invariant constant for relators: invariant_commute infrastracture
2012-04-19 kuncar 2012-04-19 use tnames for bound variables in rsp thms
2012-04-18 kuncar 2012-04-18 setup_lifting: no_code switch and supoport for quotient theorems
2012-04-18 kuncar 2012-04-18 Lifting: generate more thms & note them & tuned
2012-04-17 kuncar 2012-04-17 go back to the explicit compisition of quotient theorems
2012-04-17 huffman 2012-04-17 add theory data for relator identity rules; preprocess transfer rules generated by lift_definition using relator rules
2012-04-06 huffman 2012-04-06 more robust generation of quotient rules using tactics
2012-04-06 huffman 2012-04-06 correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
2012-04-05 kuncar 2012-04-05 detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
2012-04-05 huffman 2012-04-05 lift_definition declares transfer_rule attribute
2012-04-04 kuncar 2012-04-04 support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-04 huffman 2012-04-04 lift_definition command generates transfer rule
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit