src/HOL/Library/Quotient_Option.thy
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-15 haftmann 2010-11-15 re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-09 haftmann 2010-11-09 type annotations in specifications; 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-03-14 wenzelm 2010-03-14 observe standard header format;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.