| 2010-02-19 |
Cezary Kaliszyk |
Automatic production and proving of pseudo-injectivity.
|
file |
diff |
annotate
|
| 2010-02-19 |
Cezary Kaliszyk |
Experiments for the pseudo-injectivity tactic.
|
file |
diff |
annotate
|
| 2010-02-19 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| 2010-02-19 |
Cezary Kaliszyk |
Constructing alpha_inj goal.
|
file |
diff |
annotate
|
| 2010-02-18 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
Testing auto constant lifting.
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
Changed back to original version of trm5
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
The alternate version of trm5 with additional binding. All proofs work the same.
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
Code for handling atom sets.
|
file |
diff |
annotate
|
| 2010-02-18 |
Cezary Kaliszyk |
Replace Terms by Terms2.
|
file |
diff |
annotate
| base
|
| 2010-02-18 |
Cezary Kaliszyk |
Fixed proofs in Terms2 and found a mistake in Terms.
|
file |
diff |
annotate
|
| 2010-02-17 |
Cezary Kaliszyk |
Cleaning of proofs in Terms.
|
file |
diff |
annotate
|
| 2010-02-17 |
Cezary Kaliszyk |
Testing Fv
|
file |
diff |
annotate
|
| 2010-02-17 |
Cezary Kaliszyk |
Fix the strong induction principle.
|
file |
diff |
annotate
|
| 2010-02-17 |
Cezary Kaliszyk |
Tested the Perm code; works everywhere in Terms.
|
file |
diff |
annotate
|
| 2010-02-12 |
Cezary Kaliszyk |
renamed 'as' to 'is' everywhere.
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
the lam/bla example.
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
Finished a working foo/bar.
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
fv_foo is not regular.
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
Testing foo/bar
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
Even when bv = fv it still doesn't lift.
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
Notation available locally
|
file |
diff |
annotate
|
| 2010-02-11 |
Cezary Kaliszyk |
Main renaming + fixes for new Isabelle in IntEx2.
|
file |
diff |
annotate
|
| 2010-02-10 |
Cezary Kaliszyk |
example with a respectful bn function defined over the type itself
|
file |
diff |
annotate
|
| 2010-02-10 |
Cezary Kaliszyk |
Another mistake found with OTT.
|
file |
diff |
annotate
|
| 2010-02-10 |
Cezary Kaliszyk |
Fixed rbv6, when translating to OTT.
|
file |
diff |
annotate
|
| 2010-02-10 |
Cezary Kaliszyk |
A concrete example, with a proof that rbv is not regular and
|
file |
diff |
annotate
|