quotient_def.ML
2009-11-25 Cezary Kaliszyk applic_prs
2009-11-25 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-24 Christian Urban use error instead of raising our own exception
2009-11-22 Christian Urban updated to Isabelle 22nd November
2009-11-21 Christian Urban slight tuning
2009-11-21 Christian Urban tuned
2009-11-21 Christian Urban tunded
2009-11-21 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-19 Christian Urban updated to new Isabelle
2009-11-18 Christian Urban fixed the storage of qconst definitions
2009-11-12 Christian Urban looking up data in quot_info works now (needs qualified string)
2009-11-12 Christian Urban added a container for quotient constants (does not work yet though)
2009-11-11 Cezary Kaliszyk Modifications while preparing the goal-directed version.
2009-11-06 Christian Urban updated to new Isabelle version and added a new example file
2009-11-06 Christian Urban tuned the code in quotient and quotient_def
2009-11-05 Christian Urban removed typing information from get_fun in quotient_def; *potentially* dangerous
2009-11-05 Christian Urban replaced check_term o parse_term by read_term
2009-11-05 Christian Urban merged
2009-11-04 Christian Urban more tuning
2009-11-04 Christian Urban slightly tuned
2009-11-04 Christian Urban separated the quotient_def into a separate file
less more (0) tip