Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.

compose_tac instead of rtac to avoid unification; some code cleaning.

Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.

Using APPLY_RSP1; again a little bit faster.

Fixes after big merge.

The big merge; probably non-functional.

Testing the new tactic everywhere

First version of the deterministic rep-abs-inj-tac.

Changing = to \<equiv> in case if we want to use simp.

Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac

merge

Made your version work again with LIST_REL_EQ.

the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied

removed quot argument...not all examples work anymore

merged

merged

first version of internalised quotient theorems; added FIXME-TODO

further dead code

Reintroduced varifyT; we still need it for permutation definition.

Updated the examples

Fixed previous mistake

defs used automatically by clean_tac

Added qoutient_consts dest for getting all the constant definitions in the cleaning step.

Added the definition to quotient constant data.

removing unused code

merged

deleted some dead code

Included all_prs and ex_prs in the lambda_prs conversion.

further simplification

simplified lambda_prs_conv