LamEx.thy
2009-12-04 Cezary Kaliszyk Cleaning the Quotients file
2009-12-04 Cezary Kaliszyk merged
2009-12-04 Cezary Kaliszyk Fixes after big merge.
2009-12-04 Cezary Kaliszyk The big merge; probably non-functional.
2009-12-04 Cezary Kaliszyk Testing the new tactic everywhere
2009-12-04 Cezary Kaliszyk Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
2009-12-04 Cezary Kaliszyk Made your version work again with LIST_REL_EQ.
2009-12-03 Cezary Kaliszyk Reintroduced varifyT; we still need it for permutation definition.
2009-12-03 Cezary Kaliszyk Updated the examples
2009-12-02 Cezary Kaliszyk Experiments with OPTION_map
2009-11-30 Cezary Kaliszyk Code cleaning.
2009-11-29 Cezary Kaliszyk Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
2009-11-28 Christian Urban renamed r_mk_comb_tac to inj_repabs_tac
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Recommit
less more (0) -15 tip