src/HOL/Library/Quotient_Sum.thy
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-23 kuncar 2012-03-23 store the relational theorem for every relator
2011-12-09 kuncar 2011-12-09 Quotient_Info stores only relation maps
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-11-30 haftmann 2010-11-30 more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-18 haftmann 2010-11-18 mapper for sum type
2010-11-15 haftmann 2010-11-15 re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-09 haftmann 2010-11-09 more appropriate specification packages; fun_rel_def is no simp rule by default
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-03-14 wenzelm 2010-03-14 observe standard header format;
2010-02-19 wenzelm 2010-02-19 fixed document;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.