# HG changeset patch
# User nipkow
# Date 1537710139 -7200
# Node ID 2ce9bc515a64151b0d0fb86197682b7be7f3bca3
# Parent  8d8fdbc02912680bf4fd66d378911c2a46de2636
more standard syntax

diff -r 8d8fdbc02912 -r 2ce9bc515a64 src/HOL/GCD.thy
--- 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)"
diff -r 8d8fdbc02912 -r 2ce9bc515a64 src/HOL/Library/Complete_Partial_Order2.thy
--- 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"