Thu, 11 Mar 2010 11:32:37 +0100 |
Cezary Kaliszyk |
Lifting constants works for all examples.
|
changeset |
files
|
Thu, 11 Mar 2010 11:25:56 +0100 |
Cezary Kaliszyk |
Remove tracing from fv/alpha.
|
changeset |
files
|
Thu, 11 Mar 2010 11:25:18 +0100 |
Cezary Kaliszyk |
Equivp working only on the standard alpha-equivalences.
|
changeset |
files
|
Thu, 11 Mar 2010 11:20:50 +0100 |
Cezary Kaliszyk |
explicit cheat_fv_eqvt
|
changeset |
files
|
Thu, 11 Mar 2010 11:15:14 +0100 |
Cezary Kaliszyk |
extract build_eqvts_tac.
|
changeset |
files
|
Thu, 11 Mar 2010 10:39:29 +0100 |
Cezary Kaliszyk |
build_eqvts no longer requires permutations.
|
changeset |
files
|
Thu, 11 Mar 2010 10:22:24 +0100 |
Cezary Kaliszyk |
Add explicit alpha_eqvt_cheat.
|
changeset |
files
|
Thu, 11 Mar 2010 10:10:23 +0100 |
Cezary Kaliszyk |
Export tactic out of alpha_eqvt.
|
changeset |
files
|
Wed, 10 Mar 2010 16:59:08 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Wed, 10 Mar 2010 16:58:14 +0100 |
Cezary Kaliszyk |
More tries about the proofs in trm5
|
changeset |
files
|
Wed, 10 Mar 2010 16:51:15 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Wed, 10 Mar 2010 16:50:42 +0100 |
Christian Urban |
almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
|
changeset |
files
|