--- 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
--- 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
--- 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)