changeset 40542 | 9a173a22771c |
parent 40464 | e1db06cf6254 |
child 40820 | fd9c98ead9a9 |
--- a/src/HOL/Library/Quotient_Option.thy Mon Nov 15 14:14:38 2010 +0100 +++ b/src/HOL/Library/Quotient_Option.thy Mon Nov 15 14:59:21 2010 +0100 @@ -9,7 +9,7 @@ begin fun - option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool" + option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" where "option_rel R None None = True" | "option_rel R (Some x) None = False"