src/HOL/Lifting.thy
2015-03-16 traytel 2015-03-16 BNF relators preserve reflexivity
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-06-27 blanchet 2014-06-27 merged two small theory files
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-04-10 kuncar 2014-04-10 tuned
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-25 kuncar 2014-02-25 new rule for making rsp theorem more readable
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-20 kuncar 2014-02-20 refactoring; generate rep_eq always, not only when it would be accepted by the code generator
2014-02-20 noschinl 2014-02-20 less flex-flex pairs
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-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2013-09-27 kuncar 2013-09-27 new parametricity rules and useful lemmas
2013-09-27 Andreas Lochbihler 2013-09-27 add lemmas
2013-09-26 Andreas Lochbihler 2013-09-26 add lemmas
2013-09-16 kuncar 2013-09-16 restoring Transfer/Lifting context
2013-08-28 kuncar 2013-08-28 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
2013-08-23 kuncar 2013-08-23 remove OP
2013-08-13 kuncar 2013-08-13 introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
2013-06-05 kuncar 2013-06-05 more reflexivity rules (for OO)
2013-05-16 kuncar 2013-05-16 reflexivity rules for the function type and equality
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-05-13 kuncar 2013-05-13 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-03-08 kuncar 2013-03-08 lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-05-24 kuncar 2012-05-24 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
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-16 kuncar 2012-05-16 infrastructure that makes possible to prove that a relation is reflexive
2012-05-04 huffman 2012-05-04 lifting package produces abs_eq_iff rules for total quotients
2012-04-26 kuncar 2012-04-26 use a quot_map theorem attribute instead of the complicated map attribute
2012-04-23 kuncar 2012-04-23 move MRSL to a separate file
2012-04-21 huffman 2012-04-21 move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose
2012-04-21 huffman 2012-04-21 tuned proofs
2012-04-19 huffman 2012-04-19 generate abs_induct rules for quotient types
2012-04-18 kuncar 2012-04-18 Lifting: generate more thms & note them & tuned
2012-04-18 huffman 2012-04-18 move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients
2012-04-18 huffman 2012-04-18 add lemma Quotient_abs_induct
2012-04-18 huffman 2012-04-18 more usage of context blocks
2012-04-18 huffman 2012-04-18 use context block
2012-04-18 huffman 2012-04-18 lifting_setup generates transfer rule for rep of typedefs
2012-04-18 huffman 2012-04-18 use context block to organize typedef lifting theorems
2012-04-17 kuncar 2012-04-17 tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
2012-04-16 kuncar 2012-04-16 leave Lifting prefix
2012-04-12 bulwahn 2012-04-12 merged
2012-04-04 griff 2012-04-04 manual merge
2012-04-05 huffman 2012-04-05 add transfer lemmas for quotients
2012-04-04 huffman 2012-04-04 merged
2012-04-04 huffman 2012-04-04 add lemmas for generating transfer rules for typedefs
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 update keywords file
2012-04-04 huffman 2012-04-04 lift_definition command generates transfer rule
2012-04-03 huffman 2012-04-03 new transfer proof method
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit