src/HOL/Library/Quotient_Product.thy
changeset 40541 7850b4cc1507
parent 40465 2989f9f3aa10
child 40607 30d512bf47a7
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Mon Nov 15 00:20:36 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Mon Nov 15 14:14:38 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     1.8 +  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
     1.9  where
    1.10    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.11