Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned op's
authornipkow
Wed, 20 Dec 2017 14:53:34 +0100
changeset 67229 4ecf0ef70efb
parent 67228 7c7b76695c90
child 67230 b2800da9eb8a
tuned op's
src/HOL/Lifting.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle