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.