nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 13:46:36 +0100] rev 358

explicit phases for the cleaning

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 12:25:04 +0100] rev 357

Separate regularize_tac

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 08:36:28 +0100] rev 356

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.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 08:35:04 +0100] rev 355

More fixes for inj_REPABS

Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 01:36:50 +0100] rev 354

addded a tactic, which sets up the three goals of the `algorithm'

Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 23:09:03 +0100] rev 353

fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)

Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 22:00:54 +0100] rev 352

merged

nominal2