Quot/quotient_info.ML
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
2010-02-10 Christian Urban removed dead code
2010-02-09 Cezary Kaliszyk 'exc' -> 'exn' and more name and space cleaning.
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-02-04 Cezary Kaliszyk Quotdata_dest needed for lifting theorem translation.
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-14 Christian Urban trivial
2010-01-14 Cezary Kaliszyk Simplified matches_typ.
2010-01-14 Cezary Kaliszyk produce defs with lthy, like prs and ids
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 Christian Urban one more item in the list of Markus
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-11 Cezary Kaliszyk removed quotdata_lookup_type
2010-01-11 Cezary Kaliszyk Fix for testing matching constants in regularize.
2010-01-02 Christian Urban added a warning to the quotient_type definition, if a map function is missing
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-30 cu some small changes
2009-12-27 Christian Urban added a functor that allows checking what is added to the theorem lists
2009-12-26 Christian Urban tuned
2009-12-23 Christian Urban used Local_Theory.declaration for storing quotdata
2009-12-23 Christian Urban renamed some fields in the info records
2009-12-22 Christian Urban added "Highest Priority" category; and tuned slightly code
2009-12-22 Christian Urban added a print_maps command; updated the keyword file accordingly
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-17 Christian Urban minor cleaning
2009-12-15 Christian Urban some commenting
2009-12-10 Christian Urban added maps-printout and tuned some comments
2009-12-09 Christian Urban more proofs in IntEx2
2009-12-09 Cezary Kaliszyk Exception handling.
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-08 Christian Urban properly set up the prs_rules
2009-12-08 Christian Urban changed names of attributes
2009-12-08 Christian Urban added a thm list for ids
2009-12-08 Christian Urban removed a fixme: map_info is now checked
2009-12-07 Christian Urban final move
less more (0) tip