Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 12:26:24 +0100] rev 1416
Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:41:27 +0100] rev 1415
Proper error message.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:32:37 +0100] rev 1414
Lifting constants works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:56 +0100] rev 1413
Remove tracing from fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:18 +0100] rev 1412
Equivp working only on the standard alpha-equivalences.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:20:50 +0100] rev 1411
explicit cheat_fv_eqvt
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)