tuned op
authornipkow
Sat Jan 06 10:08:11 2018 +0100 (19 months ago)
changeset 673449a0bb8e2be07
parent 67343 f0f13aa282f4
child 67345 debef21cbed6
tuned op
src/HOL/Algebra/IntRing.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Jan 06 09:39:57 2018 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 06 10:08:11 2018 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
     1.5  
     1.6  abbreviation int_ring :: "int ring" ("\<Z>")
     1.7 -  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
     1.8 +  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
     1.9  
    1.10  lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
    1.11    by simp