Nominal/Rsp.thy
2010-05-17 Cezary Kaliszyk alpha_alphabn for bindings in a type under bn.
2010-05-12 Cezary Kaliszyk include set_simps and append_simps in fv_rsp
2010-05-12 Cezary Kaliszyk Move alpha_eqvt to unused.
2010-05-12 Cezary Kaliszyk merge
2010-05-12 Cezary Kaliszyk fvbv_rsp include prod_rel.simps
2010-05-12 Cezary Kaliszyk Use raw_induct instead of induct
2010-05-06 Cezary Kaliszyk alpha_eqvt_tac with prod_rel and prod_fv simps
2010-05-06 Cezary Kaliszyk prod_rel and prod_fv simps
2010-05-03 Cezary Kaliszyk alpha_eqvt_tac fixed to work when the existential is not at the top level.
2010-04-19 Christian Urban deleting function perm_arg in favour of the library function mk_perm
2010-04-19 Cezary Kaliszyk Accept non-equality eqvt rules in support proofs.
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Initial proof modifications for alpha_res
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
2010-03-22 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat.
2010-03-22 Cezary Kaliszyk alpha_bn_rsp_pre automatized.
2010-03-22 Cezary Kaliszyk fv_rsp proved automatically.
2010-03-20 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
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