Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
re-generalized type of prod_rel (accident from 2989f9f3aa10)
authorhaftmann
Mon, 15 Nov 2010 14:14:38 +0100
changeset 40541 7850b4cc1507
parent 40540 293f9f211be0
child 40542 9a173a22771c
re-generalized type of prod_rel (accident from 2989f9f3aa10)
src/HOL/Library/Quotient_Product.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Quotient_Product.thy	Mon Nov 15 00:20:36 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Mon Nov 15 14:14:38 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 definition
-  prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
 where
   "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
isabelle