tuned op's
authornipkow
Wed Dec 20 14:53:34 2017 +0100 (17 months ago)
changeset 672294ecf0ef70efb
parent 67228 7c7b76695c90
child 67230 b2800da9eb8a
tuned op's
src/HOL/Lifting.thy
     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: