--- a/src/HOL/List.thy Sun Jul 06 10:01:32 2025 +0200
+++ b/src/HOL/List.thy Tue Jul 08 19:13:44 2025 +0200
@@ -8502,45 +8502,6 @@
"wf_code (set xs) = acyclic (set xs)"
unfolding wf_code_def using wf_set .
-text \<open>\<open>LEAST\<close> and \<open>GREATEST\<close> operator.\<close>
-
-context
-begin
-
-qualified definition Least :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
- where Least_eq [code_abbrev, simp]: \<open>Least S = (LEAST x. x \<in> S)\<close>
-
-qualified lemma Least_filter_eq [code_abbrev]:
- \<open>Least (Set.filter P S) = (LEAST x. x \<in> S \<and> P x)\<close>
- by simp
-
-qualified definition Least_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
- where \<open>Least_abort = Least\<close>
-
-declare [[code abort: Least_abort]]
-
-qualified lemma Least_code [code]:
- \<open>Least A = (if finite A \<longrightarrow> Set.is_empty A then Least_abort A else Min A)\<close>
- using Least_Min [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Least_abort_def)
-
-qualified definition Greatest :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
- where Greatest_eq [code_abbrev, simp]: \<open>Greatest S = (GREATEST x. x \<in> S)\<close>
-
-qualified lemma Greatest_filter_eq [code_abbrev]:
- \<open>Greatest (Set.filter P S) = (GREATEST x. x \<in> S \<and> P x)\<close>
- by simp
-
-qualified definition Greatest_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
- where \<open>Greatest_abort = Greatest\<close>
-
-declare [[code abort: Greatest_abort]]
-
-qualified lemma Greatest_code [code]:
- \<open>Greatest A = (if finite A \<longrightarrow> Set.is_empty A then Greatest_abort A else Max A)\<close>
- using Greatest_Max [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Greatest_abort_def)
-
-end
-
subsubsection \<open>Pretty lists\<close>