# HG changeset patch
# User nipkow
# Date 1515584103 -3600
# Node ID 172a02125bface80b6986cc0e173a2e651dfebd3
# Parent  b39d596b77cef50b64038fbf2ef301dc0eef4413
tuned op's

diff -r b39d596b77ce -r 172a02125bfa src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Tue Jan 09 20:15:36 2018 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Wed Jan 10 12:35:03 2018 +0100
@@ -172,27 +172,27 @@
   by simp_all
 
 interpretation int (* FIXME [unfolded UNIV] *) :
-  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
-  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
-    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
-    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
+  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
+  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
+    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
+    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
 proof -
-  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
+  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
     by standard simp_all
-  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
+  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
     by simp
-  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
+  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
     by simp
-  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
+  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
     by (simp add: lless_def) auto
 qed
 
 interpretation int (* FIXME [unfolded UNIV] *) :
-  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
-  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
-    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
+  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
+  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = max x y"
+    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = min x y"
 proof -
-  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
+  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
   show "lattice ?Z"
     apply unfold_locales
     apply (simp add: least_def Upper_def)
@@ -214,7 +214,7 @@
 qed
 
 interpretation int (* [unfolded UNIV] *) :
-  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
+  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
   by standard clarsimp
 
 
diff -r b39d596b77ce -r 172a02125bfa src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Jan 09 20:15:36 2018 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Jan 10 12:35:03 2018 +0100
@@ -1808,7 +1808,7 @@
 
 definition
   INTEG :: "int ring"
-  where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+  where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
diff -r b39d596b77ce -r 172a02125bfa src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 09 20:15:36 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jan 10 12:35:03 2018 +0100
@@ -5942,7 +5942,7 @@
     apply (blast intro: fg)
     done
   also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
-      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op*u", unfolded o_def])
+      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op* u", unfolded o_def])
       apply (rule derivative_intros)
       using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
       apply (simp add: deriv_linear)