src/HOL/Tools/Quotient/quotient_typ.ML
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-19 wenzelm 2010-03-19 typedef etc.: no constraints;
2010-03-16 Christian Urban 2010-03-16 rollback of local typedef until problem with type-variables can be sorted out; fixed header
2010-03-14 Christian Urban 2010-03-14 removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14 wenzelm 2010-03-14 observe standard header format;
2010-03-13 wenzelm 2010-03-13 global typedef;
2010-03-01 Cezary Kaliszyk 2010-03-01 export add_quotient_type.
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.