| changeset 539 | 8287fb5b8d7a |
| parent 537 | 57073b0b8fac |
| child 540 | c0b13fb70d6d |
| 538:bce41bea3de2 | 539:8287fb5b8d7a |
|---|---|
459 ML {* |
459 ML {* |
460 fun equiv_tac rel_eqvs = |
460 fun equiv_tac rel_eqvs = |
461 REPEAT_ALL_NEW (FIRST' |
461 REPEAT_ALL_NEW (FIRST' |
462 [resolve_tac rel_eqvs, |
462 [resolve_tac rel_eqvs, |
463 rtac @{thm IDENTITY_equivp}, |
463 rtac @{thm IDENTITY_equivp}, |
464 rtac @{thm LIST_equivp}]) |
464 rtac @{thm list_equivp}]) |
465 *} |
465 *} |
466 |
466 |
467 ML {* |
467 ML {* |
468 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
468 fun ball_reg_eqv_simproc rel_eqvs ss redex = |
469 let |
469 let |