# HG changeset patch
# User nipkow
# Date 1513778014 -3600
# Node ID 4ecf0ef70efb3e8bfa1f1ece38ddfc2bb3bb72c3
# Parent  7c7b76695c9078ad9e4b9a85b9cbbff0c7bd18fb
tuned op's

diff -r 7c7b76695c90 -r 4ecf0ef70efb src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Dec 20 12:22:36 2017 +0100
+++ b/src/HOL/Lifting.thy	Wed Dec 20 14:53:34 2017 +0100
@@ -228,7 +228,7 @@
   fixes Abs :: "'a \<Rightarrow> 'b"
   and Rep :: "'b \<Rightarrow> 'a"
   assumes "type_definition Rep Abs (UNIV::'a set)"
-  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+  shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
 by (rule identity_equivp)
 
 lemma typedef_to_Quotient: