src/HOL/Library/Quotient_List.thy
2011-12-09 kuncar 2011-12-09 Quotient_Info stores only relation maps
2010-11-30 haftmann 2010-11-30 more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-09 haftmann 2010-11-09 fun_rel_def is no simp rule by default
2010-10-19 bulwahn 2010-10-19 removing something that probably slipped into the Quotient_List theory
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-06-23 Cezary Kaliszyk 2010-06-23 Replace 'list_rel' by 'list_all2'; they are equivalent.
2010-05-11 Christian Urban 2010-05-11 tuned proof so that no simplifier warning is printed
2010-04-22 Cezary Kaliszyk 2010-04-22 fun_rel introduction and list_rel elimination for quotient package
2010-04-20 Cezary Kaliszyk 2010-04-20 respectfullness and preservation of map for identity quotients
2010-04-15 Cezary Kaliszyk 2010-04-15 Respectfullness and preservation of list_rel
2010-03-14 wenzelm 2010-03-14 observe standard header format;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.