nominal2: Changelog

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.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 11:06:43 +0100] rev 518

compose_tac instead of rtac to avoid unification; some code cleaning.

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

Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.

nominal2