src/HOL/Lifting.thy
changeset 67229 4ecf0ef70efb
parent 63343 fb5d8a50c641
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Lifting.thy	Wed Dec 20 12:22:36 2017 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Wed Dec 20 14:53:34 2017 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4    fixes Abs :: "'a \<Rightarrow> 'b"
     1.5    and Rep :: "'b \<Rightarrow> 'a"
     1.6    assumes "type_definition Rep Abs (UNIV::'a set)"
     1.7 -  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
     1.8 +  shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
     1.9  by (rule identity_equivp)
    1.10  
    1.11  lemma typedef_to_Quotient: