Nominal/Rsp.thy
2010-03-18 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser.
2010-03-17 Cezary Kaliszyk Finished all proofs in Term5 and Term5n.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-11 Cezary Kaliszyk Lifting constants.
2010-03-11 Cezary Kaliszyk extract build_eqvts_tac.
2010-03-11 Cezary Kaliszyk build_eqvts no longer requires permutations.
2010-03-11 Cezary Kaliszyk Export tactic out of alpha_eqvt.
2010-03-03 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-02 Cezary Kaliszyk Include the raw eqvt lemmas.
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Cezary Kaliszyk Fixed eqvt code.
2010-02-26 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
2010-02-25 Cezary Kaliszyk Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25 Christian Urban moved Nominal to "toplevel"
less more (0) tip