src/HOL/Lifting_Set.thy
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