equal
deleted
inserted
replaced
508 |
508 |
509 (* Not used *) |
509 (* Not used *) |
510 lemma rep_abs_rsp_left: |
510 lemma rep_abs_rsp_left: |
511 assumes q: "Quotient R Abs Rep" |
511 assumes q: "Quotient R Abs Rep" |
512 and a: "R x1 x2" |
512 and a: "R x1 x2" |
513 shows "R x1 (Rep (Abs x2))" |
513 shows "R (Rep (Abs x1)) x2" |
514 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
514 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
515 |
515 |
516 |
516 |
517 |
517 |
518 (* bool theory: COND, LET *) |
518 (* bool theory: COND, LET *) |