quotient_info.ML
2009-12-03 Christian Urban merged
2009-12-03 Christian Urban first version of internalised quotient theorems; added FIXME-TODO
2009-12-03 Cezary Kaliszyk Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
2009-12-03 Cezary Kaliszyk Added the definition to quotient constant data.
2009-11-30 Christian Urban added facilities to get all stored quotient data (equiv thms etc)
2009-11-29 Christian Urban introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-27 Christian Urban deleted obsolete qenv code
2009-11-21 Christian Urban slight tuning
2009-11-21 Christian Urban tunded
2009-11-21 Christian Urban flagged qenv-stuff as obsolete
2009-11-21 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-20 Christian Urban started regularize of rtrm/qtrm version; looks quite promising
2009-11-18 Christian Urban fixed the storage of qconst definitions
2009-11-12 Cezary Kaliszyk merged
2009-11-12 Christian Urban changed the quotdata to be a symtab table (needs fixing)
2009-11-12 Christian Urban added a container for quotient constants (does not work yet though)
2009-11-11 Christian Urban updated to new Theory_Data and to new Isabelle
2009-11-03 Christian Urban simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-02 Christian Urban split quotient.ML into two files
less more (0) tip