src/HOL/Library/Quotient_Product.thy
changeset 58916 229765cc3414
parent 58881 b9556a055632
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Nov 07 12:24:56 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Nov 07 11:28:37 2014 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  lemma [quot_respect]:
     1.5    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
     1.6    rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod"
     1.7 -  by (rule rel_prod_transfer)
     1.8 +  by (rule prod.rel_transfer)
     1.9  
    1.10  lemma [quot_preserve]:
    1.11    assumes q1: "Quotient3 R1 abs1 rep1"