Quot/quotient_typ.ML
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-24 Christian Urban test with splits
2010-01-14 Christian Urban tuned quotient_typ.ML
2010-01-13 Christian Urban one more item in the list of Markus
2010-01-12 Cezary Kaliszyk More indenting, bracket removing and comment restructuring.
2010-01-11 Christian Urban started to adhere to Wenzel-Standard
2010-01-02 Christian Urban added a warning to the quotient_type definition, if a map function is missing
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-26 Christian Urban tuned
2009-12-26 Christian Urban generalised absrep function; needs consolidation
2009-12-24 Christian Urban tuned
2009-12-24 Christian Urban added sanity checks for quotient_type
2009-12-24 Christian Urban made the quotient_type definition more like typedef; now type variables need to be explicitly given
2009-12-23 Christian Urban used Local_Theory.declaration for storing quotdata
2009-12-23 Christian Urban modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
2009-12-23 Christian Urban cleaed a bit function mk_typedef_main
2009-12-23 Christian Urban renamed QUOT_TYPE to Quot_Type
2009-12-23 Christian Urban explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
2009-12-19 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-19 Christian Urban avoided global "open"s - replaced by local "open"s
2009-12-19 Christian Urban various tunings; map_lookup now raises an exception; addition to FIXME-TODO
2009-12-12 Christian Urban renamed quotient.ML to quotient_typ.ML
less more (0) tip