Quot/Nominal/LFex.thy
2010-02-24 Cezary Kaliszyk Use the infrastructure in LF. Much shorter :).
2010-02-24 Cezary Kaliszyk Final synchronization of names.
2010-02-24 Cezary Kaliszyk LF renaming part 3 (proper names of alpha equvalences)
2010-02-24 Cezary Kaliszyk LF renaming part 2 (proper fv functions)
2010-02-24 Cezary Kaliszyk LF renaming part1.
2010-02-23 Cezary Kaliszyk All works in LF but will require renaming.
2010-02-23 Cezary Kaliszyk Reordering in LF.
2010-02-22 Cezary Kaliszyk Generalize atom_trans and atom_sym.
2010-02-12 Cezary Kaliszyk renamed 'as' to 'is' everywhere.
2010-02-11 Cezary Kaliszyk Notation available locally
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
2010-02-08 Cezary Kaliszyk Proper context fixes lifting inside instantiations.
2010-02-08 Cezary Kaliszyk Fixed the context import/export and simplified LFex.
2010-02-03 Christian Urban another adaptation for the eqvt-change
2010-02-03 Cezary Kaliszyk The alpha-equivalence relation for let-rec. Not sure if correct...
2010-02-02 Cezary Kaliszyk LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
2010-02-02 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
2010-02-02 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction.
2010-02-01 Cezary Kaliszyk The current state of fv vs supp proofs in LF.
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases.
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
less more (0) tip