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