Nominal/Parser.thy
2010-03-11 Cezary Kaliszyk build_eqvts no longer requires permutations.
2010-03-11 Cezary Kaliszyk Add explicit alpha_eqvt_cheat.
2010-03-11 Cezary Kaliszyk Export tactic out of alpha_eqvt.
2010-03-10 Christian Urban merged
2010-03-10 Christian Urban almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10 Cezary Kaliszyk Undoing mistakenly committed parser experiments.
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-08 Christian Urban merged
2010-03-08 Christian Urban updated to new Isabelle
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
less more (0) -14 tip