2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-03-29 wenzelm 2015-03-29 clarified equality of formal entities;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2012-04-23 kuncar 2012-04-23 move MRSL to a separate file
2012-04-17 kuncar 2012-04-17 go back to the explicit compisition of quotient theorems
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-23 kuncar 2012-03-23 use Thm.transfer for thms stored in generic context data storage
2012-03-23 kuncar 2012-03-23 generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
2012-03-23 kuncar 2012-03-23 simplified code of generation of aggregate relations
2012-02-05 Cezary Kaliszyk 2012-02-05 Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2011-12-09 kuncar 2011-12-09 make ctxt the first parameter
2011-12-09 kuncar 2011-12-09 context/theory parametres tuned
2011-12-09 kuncar 2011-12-09 maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
2011-11-25 Christian Urban 2011-11-25 in a local context, also the free variable case needs to be analysed default tip
2011-11-17 bulwahn 2011-11-17 adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
2011-11-04 wenzelm 2011-11-04 prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
2011-10-27 wenzelm 2011-10-27 localized quotient data;
2011-10-27 wenzelm 2011-10-27 simplified/standardized signatures;
2011-10-27 bulwahn 2011-10-27 respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception
2011-10-27 bulwahn 2011-10-27 respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
2011-10-27 bulwahn 2011-10-27 respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
2011-08-23 Cezary Kaliszyk 2011-08-23 Quotient Package: some infrastructure for lifting inside sets
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2011-01-07 wenzelm 2011-01-07 more precise parentheses and indentation; eliminated trailing whitespace;
2010-10-28 wenzelm 2010-10-28 handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable; clarified handle/raise wrt. Quotient_Info.NotFound -- avoid fragile unqualified NotFound depending on "open" scope; added helpful comments;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-25 Christian Urban 2010-08-25 tuned code
2010-08-24 Christian Urban 2010-08-24 use matching of types than just equality - this is needed in nominal to cope with type variables
2010-08-22 Christian Urban 2010-08-22 changed to a more convenient argument order
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-07-08 haftmann 2010-07-08 tuned titles
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-29 Christian Urban 2010-06-29 tuned
2010-06-28 Christian Urban 2010-06-28 separation of translations in derive_qtrm / derive_rtrm (similarly for types)
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-28 Cezary Kaliszyk 2010-06-28 Quotient package reverse lifting
2010-06-28 Cezary Kaliszyk 2010-06-28 Add reverse lifting flag to automated theorem derivation
2010-06-26 Christian Urban 2010-06-26 streamlined the generation of quotient theorems out of raw theorems
2010-06-24 Christian Urban 2010-06-24 slight cleaning and simplification of the automatic wrapper for quotient definitions
2010-06-24 Christian Urban 2010-06-24 export of proper information in the ML-interface of the quotient package
2010-05-26 haftmann 2010-05-26 normalized references to constant "split"
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-27 Cezary Kaliszyk 2010-03-27 Automated lifting can be restricted to specific quotient types
2010-03-19 Cezary Kaliszyk 2010-03-19 Check that argument is not a 'Bound' before calling fastype_of.
2010-03-14 wenzelm 2010-03-14 observe standard header format;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.