Quot/quotient_term.ML
Thu, 21 Jan 2010 10:55:09 +0100 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
Thu, 21 Jan 2010 07:38:34 +0100 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
Wed, 20 Jan 2010 16:44:31 +0100 Cezary Kaliszyk Better error messages for non matching quantifiers.
Fri, 15 Jan 2010 15:51:25 +0100 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Fri, 15 Jan 2010 12:17:30 +0100 Christian Urban slight tuning of relation_error
Thu, 14 Jan 2010 16:41:17 +0100 Cezary Kaliszyk exported absrep_const for nitpick.
less more (0) -30 -10 -6 tip