src/HOL/Lifting.thy
5 weeks ago wenzelm 2019-03-14 more specific keyword kinds;
3 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
16 months ago nipkow 2017-12-20 tuned op's
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
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
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