Wed, 25 Nov 2009 12:27:28 +0100 Christian Urban comments tuning and slight reordering
Wed, 25 Nov 2009 11:59:49 +0100 Cezary Kaliszyk Merge
Wed, 25 Nov 2009 11:58:56 +0100 Cezary Kaliszyk More moving from QuotMain to UnusedQuotMain
Wed, 25 Nov 2009 11:46:59 +0100 Christian Urban deleted some obsolete diagnostic code
Wed, 25 Nov 2009 11:41:42 +0100 Cezary Kaliszyk Removed unused things from QuotMain.
Wed, 25 Nov 2009 10:52:21 +0100 Cezary Kaliszyk All examples work again.
Wed, 25 Nov 2009 10:39:53 +0100 Cezary Kaliszyk cleaning in MyInt
Wed, 25 Nov 2009 10:34:03 +0100 Cezary Kaliszyk lambda_prs and cleaning the existing examples.
Wed, 25 Nov 2009 03:47:07 +0100 Christian Urban merged
Wed, 25 Nov 2009 03:45:44 +0100 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
Tue, 24 Nov 2009 20:13:16 +0100 Cezary Kaliszyk Ho-matching failures...
Tue, 24 Nov 2009 19:09:29 +0100 Christian Urban changed unification to matching
Tue, 24 Nov 2009 18:13:57 +0100 Christian Urban unification
Tue, 24 Nov 2009 18:13:18 +0100 Cezary Kaliszyk Lambda & SOLVED' for new quotient_tac
Tue, 24 Nov 2009 17:35:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 17:00:53 +0100 Cezary Kaliszyk Conversion
Tue, 24 Nov 2009 16:20:34 +0100 Cezary Kaliszyk The non-working procedure_tac.
Tue, 24 Nov 2009 16:10:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:31:29 +0100 Christian Urban use error instead of raising our own exception
Tue, 24 Nov 2009 15:18:00 +0100 Cezary Kaliszyk Fixes to the tactic after quotient_tac changed.
Tue, 24 Nov 2009 15:15:33 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:15:10 +0100 Christian Urban added a prepare_tac
Tue, 24 Nov 2009 14:41:47 +0100 Cezary Kaliszyk TRY' for clean_tac
Tue, 24 Nov 2009 14:19:54 +0100 Cezary Kaliszyk Moved cleaning to QuotMain
Tue, 24 Nov 2009 14:16:57 +0100 Cezary Kaliszyk New cleaning tactic
Tue, 24 Nov 2009 13:46:36 +0100 Christian Urban explicit phases for the cleaning
Tue, 24 Nov 2009 12:25:04 +0100 Cezary Kaliszyk Separate regularize_tac
Tue, 24 Nov 2009 08:36:28 +0100 Cezary Kaliszyk Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Tue, 24 Nov 2009 08:35:04 +0100 Cezary Kaliszyk More fixes for inj_REPABS
Tue, 24 Nov 2009 01:36:50 +0100 Christian Urban addded a tactic, which sets up the three goals of the `algorithm'
(0) -300 -100 -50 -30 +30 +50 +100 +300 +1000 tip