Nominal/Parser.thy
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 Cezary Kaliszyk Lifting theorems with compound fv and compound alpha.
2010-03-16 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
less more (0) -30 -10 -3 tip