equal
deleted
inserted
replaced
518 |
518 |
519 3. simplification with: |
519 3. simplification with: |
520 |
520 |
521 - Quotient_abs_rep Quotient_rel_rep |
521 - Quotient_abs_rep Quotient_rel_rep |
522 babs_prs all_prs ex_prs ex1_prs |
522 babs_prs all_prs ex_prs ex1_prs |
523 - id_simps |
523 |
524 |
524 - id_simps and preservation lemmas and |
525 and folding of definitions and preservation lemmas |
525 |
|
526 - symmetric versions of the definitions |
|
527 (that is definitions of quotient constants |
|
528 are folded) |
526 |
529 |
527 4. test for refl |
530 4. test for refl |
528 *) |
531 *) |
529 fun clean_tac lthy = |
532 fun clean_tac lthy = |
530 let |
533 let |