nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:04:05 +0100] rev 528

Naming changes

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:35:36 +0100] rev 527

code cleaning and renaming

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:20 +0100] rev 526

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:03 +0100] rev 525

Removed previous inj_repabs_tac

Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 13:58:23 +0100] rev 524

some tuning

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 12:21:15 +0100] rev 523

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 12:20:49 +0100] rev 522

rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.

Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:49 +0100] rev 521

merged

Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:21 +0100] rev 520

merged

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 11:33:58 +0100] rev 519

Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.

nominal2