nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:15:14 +0100] rev 1410

extract build_eqvts_tac.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:39:29 +0100] rev 1409

build_eqvts no longer requires permutations.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:22:24 +0100] rev 1408

Add explicit alpha_eqvt_cheat.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:10:23 +0100] rev 1407

Export tactic out of alpha_eqvt.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:59:08 +0100] rev 1406

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:58:14 +0100] rev 1405

More tries about the proofs in trm5

Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:51:15 +0100] rev 1404

merged

Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:50:42 +0100] rev 1403

almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:40:15 +0100] rev 1402

alpha_equivp for trm5

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:34:13 +0100] rev 1401

Undoing mistakenly committed parser experiments.

nominal2