equal
deleted
inserted
replaced
1127 |
1127 |
1128 lemmas [transfer_rule del] = |
1128 lemmas [transfer_rule del] = |
1129 rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer |
1129 rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer |
1130 Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer |
1130 Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer |
1131 uminus_rat.transfer times_rat.transfer inverse_rat.transfer |
1131 uminus_rat.transfer times_rat.transfer inverse_rat.transfer |
1132 positive.transfer of_rat.transfer |
1132 positive.transfer of_rat.transfer rat.right_unique rat.right_total |
1133 |
1133 |
1134 text {* De-register @{text "rat"} as a quotient type: *} |
1134 text {* De-register @{text "rat"} as a quotient type: *} |
1135 |
1135 |
1136 declare Quotient_rat[quot_del] |
1136 declare Quotient_rat[quot_del] |
1137 |
1137 |