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