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