Nominal/Ex/Lambda.thy
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases
2011-01-19 Christian Urban defined height as a function that returns an integer
2011-01-18 Christian Urban defined properly substitution
2011-01-18 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
less more (0) -30 -10 -6 tip