Nominal/Test.thy
2010-03-15 Cezary Kaliszyk fv_eqvt_cheat no longer needed.
2010-03-15 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 Cezary Kaliszyk Use eqvt.
2010-03-15 Christian Urban added an eqvt-proof for bi
2010-03-13 Christian Urban started supp-fv proofs (is going to work)
less more (0) -30 -10 -6 tip