# HG changeset patch
# User wenzelm
# Date 1733667140 -3600
# Node ID c4c983c5c7f211325d7bb1495bb62c4740b2b090
# Parent  d387683ea725845773c9f3ec7ba7e186a908bc28
tuned: prefer explicit names of inferred types;

diff -r d387683ea725 -r c4c983c5c7f2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Dec 08 14:27:06 2024 +0100
+++ b/src/HOL/Fun.thy	Sun Dec 08 15:12:20 2024 +0100
@@ -1077,7 +1077,8 @@
 end
 
 lemma mono_on_greaterD:
-  assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
+  fixes g :: "'a::linorder \<Rightarrow> 'b::linorder"
+  assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > g y"
   shows "x > y"
 proof (rule ccontr)
   assume "\<not>x > y"
@@ -1263,7 +1264,8 @@
 qed
 
 lemma strict_mono_on_imp_inj_on:
-  assumes "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder))"
+  fixes f :: "'a::linorder \<Rightarrow> 'b::preorder"
+  assumes "strict_mono_on A f"
   shows "inj_on f A"
 proof (rule inj_onI)
   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
@@ -1273,7 +1275,8 @@
 qed
 
 lemma strict_mono_on_leD:
-  assumes "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder)" "x \<in> A" "y \<in> A" "x \<le> y"
+  fixes f :: "'a::linorder \<Rightarrow> 'b::preorder"
+  assumes "strict_mono_on A f" "x \<in> A" "y \<in> A" "x \<le> y"
   shows "f x \<le> f y"
 proof (cases "x = y")
   case True
@@ -1286,13 +1289,13 @@
 qed
 
 lemma strict_mono_on_eqD:
-  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
+  fixes f :: "'c::linorder \<Rightarrow> 'd::preorder"
   assumes "strict_mono_on A f" "f x = f y" "x \<in> A" "y \<in> A"
   shows "y = x"
   using assms by (cases rule: linorder_cases) (auto dest: strict_mono_onD)
 
-lemma strict_mono_on_imp_mono_on:
-  "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
+lemma strict_mono_on_imp_mono_on: "strict_mono_on A f \<Longrightarrow> mono_on A f"
+  for f :: "'a::linorder \<Rightarrow> 'b::preorder"
   by (rule mono_onI, rule strict_mono_on_leD)
 
 lemma mono_imp_strict_mono: