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
|
Wed, 10 Mar 2010 15:40:15 +0100 |
Cezary Kaliszyk |
alpha_equivp for trm5
|
changeset |
files
|
Wed, 10 Mar 2010 15:34:13 +0100 |
Cezary Kaliszyk |
Undoing mistakenly committed parser experiments.
|
changeset |
files
|
Wed, 10 Mar 2010 15:32:51 +0100 |
Cezary Kaliszyk |
alpha_eqvt for recursive term1.
|
changeset |
files
|
Wed, 10 Mar 2010 14:47:04 +0100 |
Cezary Kaliszyk |
Looking at alpha_eqvt for term5, not much progress.
|
changeset |
files
|
Wed, 10 Mar 2010 14:24:27 +0100 |
Cezary Kaliszyk |
Reordered examples in Test.
|
changeset |
files
|
Wed, 10 Mar 2010 13:29:12 +0100 |
Cezary Kaliszyk |
Allows multiple bindings with same lhs.
|
changeset |
files
|