diff -r 99b37c391433 -r 426afab39a55 src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Mon May 30 20:58:45 2022 +0200
+++ b/src/HOL/Data_Structures/Selection.thy	Tue May 31 20:55:51 2022 +0200
@@ -4,7 +4,7 @@
 *)
 section \<open>The Median-of-Medians Selection Algorithm\<close>
 theory Selection
-  imports Complex_Main Sorting Time_Funs
+  imports Complex_Main Time_Funs Sorting
 begin
 
 text \<open>
@@ -17,8 +17,8 @@
 lemma replicate_numeral: "replicate (numeral n) x = x # replicate (pred_numeral n) x"
   by (simp add: numeral_eq_Suc)
 
-lemma isort_correct: "isort xs = sort xs"
-  using sorted_isort mset_isort by (metis properties_for_sort)
+lemma insort_correct: "insort xs = sort xs"
+  using sorted_insort mset_insort by (metis properties_for_sort)
 
 lemma sum_list_replicate [simp]: "sum_list (replicate n x) = n * x"
   by (induction n) auto
@@ -498,13 +498,13 @@
   using the naive selection algorithm where we sort the list using insertion sort.
 \<close>
 definition slow_select where
-  "slow_select k xs = isort xs ! k"
+  "slow_select k xs = insort xs ! k"
 
 definition slow_median where
   "slow_median xs = slow_select ((length xs - 1) div 2) xs"
 
 lemma slow_select_correct: "slow_select k xs = select k xs"
-  by (simp add: slow_select_def select_def isort_correct)
+  by (simp add: slow_select_def select_def insort_correct)
 
 lemma slow_median_correct: "slow_median xs = median xs"
   by (simp add: median_def slow_median_def slow_select_correct)
@@ -635,18 +635,18 @@
   by (induction x xs rule: T_partition3.induct) auto
 
 definition T_slow_select :: "nat \<Rightarrow> 'a :: linorder list \<Rightarrow> nat" where
-  "T_slow_select k xs = T_isort xs + T_nth (isort xs) k + 1"
+  "T_slow_select k xs = T_insort xs + T_nth (insort xs) k + 1"
 
 definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
   "T_slow_median xs = T_slow_select ((length xs - 1) div 2) xs + 1"
 
 lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 3"
 proof -
-  have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (isort xs) + 1) + 1"
+  have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (insort xs) + 1) + 1"
     unfolding T_slow_select_def
-    by (intro add_mono T_isort_length) (auto simp: T_nth_eq)
+    by (intro add_mono T_insort_length) (auto simp: T_nth_eq)
   also have "\<dots> = length xs ^ 2 + 3 * length xs + 3"
-    by (simp add: isort_correct algebra_simps power2_eq_square)
+    by (simp add: insort_correct algebra_simps power2_eq_square)
   finally show ?thesis .
 qed