Quot/quotient_def.ML
2010-02-10 Christian Urban merged
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Cezary Kaliszyk Finished organising an efficient datastructure for qconst_info.
2010-01-14 Cezary Kaliszyk Undid changes from symtab to termtab, since we need to lookup specialized types.
2010-01-13 Cezary Kaliszyk Better error message for definition failure.
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-13 Christian Urban tuned
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban fixed comment errors
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-24 Christian Urban tuned
2009-12-22 Christian Urban renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
2009-12-22 Christian Urban tuned
2009-12-22 Christian Urban moved get_fun into quotient_term; this simplifies the overall including structure of the package
2009-12-21 Christian Urban get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
2009-12-19 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
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-11 Cezary Kaliszyk Renaming
2009-12-11 Cezary Kaliszyk Updated comments.
2009-12-11 Cezary Kaliszyk New syntax for definitions.
2009-12-09 Christian Urban fixed minor stupidity
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-07 Christian Urban final move
less more (0) tip