QuotMain.thy
2009-12-04 Cezary Kaliszyk More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
2009-12-04 Cezary Kaliszyk Cleaning & Renaming coming from QuotList
2009-12-04 Cezary Kaliszyk Even more name changes and cleaning
2009-12-04 Cezary Kaliszyk More code cleaning and name changes
2009-12-04 Cezary Kaliszyk More name changes
2009-12-04 Cezary Kaliszyk code cleaning and renaming
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk Removed previous inj_repabs_tac
2009-12-04 Christian Urban some tuning
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04 Christian Urban merged
2009-12-04 Christian Urban merged
2009-12-04 Cezary Kaliszyk Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04 Cezary Kaliszyk compose_tac instead of rtac to avoid unification; some code cleaning.
2009-12-04 Cezary Kaliszyk Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
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 First version of the deterministic rep-abs-inj-tac.
2009-12-04 Cezary Kaliszyk Changing = to \<equiv> in case if we want to use simp.
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 merge
2009-12-04 Cezary Kaliszyk Made your version work again with LIST_REL_EQ.
2009-12-03 Christian Urban the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03 Christian Urban removed quot argument...not all examples work anymore
2009-12-03 Christian Urban merged
less more (0) -300 -100 -50 -28 tip