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
|
2010-02-09 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-02-09 |
Christian Urban |
slight correction
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
More about trm6
|
file |
diff |
annotate
|
2010-02-09 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
the specifications of the respects.
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
trm6 with the 'Foo' constructor.
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
Explicitly marked what is bound.
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
Cleaning and updating in Terms.
|
file |
diff |
annotate
|
2010-02-09 |
Cezary Kaliszyk |
Looking at the trm2 example
|
file |
diff |
annotate
|
2010-02-08 |
Cezary Kaliszyk |
Proper context fixes lifting inside instantiations.
|
file |
diff |
annotate
|
2010-02-05 |
Cezary Kaliszyk |
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
More let-rec experiments
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
proposal for an alpha equivalence
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Lets different.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Simplified the proof.
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
proved that bv for lists respects alpha for terms
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Finished remains on the let proof.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Lets are ok.
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
added type-scheme example
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Definitions for trm5
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
fixed proofs that broke because of eqvt
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Minor fix.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
alpha5 pseudo-injective
|
file |
diff |
annotate
|
2010-02-03 |
Christian Urban |
fixed proofs in Abs.thy
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
The alpha-equivalence relation for let-rec. Not sure if correct...
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Starting with a let-rec example.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
Some cleaning and eqvt proof
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
The trm1_support lemma explicitly and stated a strong induction principle.
|
file |
diff |
annotate
|
2010-02-03 |
Cezary Kaliszyk |
More ingredients in Terms.
|
file |
diff |
annotate
|
2010-02-02 |
Cezary Kaliszyk |
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
|
file |
diff |
annotate
|
2010-02-02 |
Cezary Kaliszyk |
More in Terms
|
file |
diff |
annotate
|
2010-02-02 |
Cezary Kaliszyk |
First experiments in Terms.
|
file |
diff |
annotate
|
2010-01-28 |
Christian Urban |
minor
|
file |
diff |
annotate
|
2010-01-27 |
Christian Urban |
completely ported
|
file |
diff |
annotate
|
2010-01-27 |
Christian Urban |
mostly ported Terms.thy to new Nominal
|
file |
diff |
annotate
|
2010-01-27 |
Christian Urban |
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
|
file |
diff |
annotate
|