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
authornipkow
Sat, 06 Jan 2018 10:08:11 +0100
changeset 67344 9a0bb8e2be07
parent 67343 f0f13aa282f4
child 67345 debef21cbed6
tuned op
src/HOL/Algebra/IntRing.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Algebra/IntRing.thy	Sat Jan 06 09:39:57 2018 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 06 10:08:11 2018 +0100
@@ -23,7 +23,7 @@
 subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
 
 abbreviation int_ring :: "int ring" ("\<Z>")
-  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
 
 lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
   by simp
isabelle