Quot/Nominal/Fv.thy
2010-02-23 Cezary Kaliszyk Minor beutification.
2010-02-23 Cezary Kaliszyk Fixes for auxiliary datatypes.
2010-02-22 Cezary Kaliszyk Fixed pseudo_injectivity for trm4
2010-02-22 Cezary Kaliszyk Testing auto equivp code.
2010-02-22 Cezary Kaliszyk A tactic for final equivp
2010-02-22 Cezary Kaliszyk More equivp infrastructure.
2010-02-22 Cezary Kaliszyk Some progress about transp
2010-02-22 Cezary Kaliszyk alpha-symmetric addons.
2010-02-22 Cezary Kaliszyk alpha reflexivity
2010-02-22 Cezary Kaliszyk Renaming.
2010-02-19 Cezary Kaliszyk Automatic production and proving of pseudo-injectivity.
2010-02-19 Cezary Kaliszyk Constructing alpha_inj goal.
2010-02-18 Cezary Kaliszyk Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18 Cezary Kaliszyk First (non-working) version of alpha-equivalence
2010-02-18 Cezary Kaliszyk Description of the fv procedure.
2010-02-18 Cezary Kaliszyk Code for handling atom sets.
2010-02-17 Cezary Kaliszyk Testing Fv
2010-02-17 Cezary Kaliszyk Reorder
2010-02-17 Cezary Kaliszyk Add bindings of recursive types by free_variables.
2010-02-17 Cezary Kaliszyk Bindings adapted to multiple defined datatypes.
2010-02-17 Cezary Kaliszyk Reorganization
2010-02-17 Cezary Kaliszyk Now should work.
2010-02-17 Cezary Kaliszyk Some optimizations and fixes.
2010-02-17 Cezary Kaliszyk Simplified format of bindings.
2010-02-17 Cezary Kaliszyk Description of intended bindings.
2010-02-17 Cezary Kaliszyk Code for generating the fv function, no bindings yet.
less more (0) tip