src/HOL/Lifting_Set.thy
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
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-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-07-21 Andreas Lochbihler 2014-07-21 add parametricity lemmas
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-04-10 kuncar 2014-04-10 setup for Transfer and Lifting from BNF; tuned thm names
2014-04-10 kuncar 2014-04-10 abstract Domainp in relator_domain rules => more natural statement of the rule
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-09 haftmann 2014-04-09 parametricity transfer rule for INFIMUM, SUPREMUM
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-02-18 kuncar 2014-02-18 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-09-27 kuncar 2013-09-27 new parametricity rules and useful lemmas
2013-09-27 Andreas Lochbihler 2013-09-27 tuned proofs
2013-09-26 Andreas Lochbihler 2013-09-26 add lemmas
2013-08-13 kuncar 2013-08-13 move Lifting/Transfer relevant parts of Library/Quotient_* to Main