Quot/quotient_term.ML
2010-01-21 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
2010-01-21 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
2010-01-20 Cezary Kaliszyk Better error messages for non matching quantifiers.
2010-01-15 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
2010-01-15 Christian Urban slight tuning of relation_error
2010-01-14 Cezary Kaliszyk exported absrep_const for nitpick.
2010-01-14 Cezary Kaliszyk Simplified matches_typ.
2010-01-13 Cezary Kaliszyk Moved the matches_typ function outside a?d simplified it.
2010-01-13 Cezary Kaliszyk Put relation_error as a separate function.
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 More indenting, bracket removing and comment restructuring.
2010-01-12 Cezary Kaliszyk modifying comments/indentation in quotient_term.ml
2010-01-11 Cezary Kaliszyk removed quotdata_lookup_type
less more (0) -15 tip