--- a/src/HOL/GCD.thy Sun Sep 23 13:45:37 2018 +0200
+++ b/src/HOL/GCD.thy Sun Sep 23 15:42:19 2018 +0200
@@ -1092,14 +1092,14 @@
sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
defines
- Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+ Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
defines
- Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
+ Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Sep 23 13:45:37 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Sep 23 15:42:19 2018 +0200
@@ -161,7 +161,7 @@
end
lemma Sup_image_mono_le:
- fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
+ fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>")
assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"