more "sorted" changes

--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue May 08 10:14:36 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue May 08 10:22:58 2018 +0200
@@ -556,7 +556,7 @@
         by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
       with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
         unfolding subarray_def
-        apply (auto simp add: sorted_append sorted_Cons all_in_set_nths'_conv)
+        apply (auto simp add: sorted_append all_in_set_nths'_conv)
         by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
     }
     with True cr show ?thesis

--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue May 08 10:14:36 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue May 08 10:22:58 2018 +0200
@@ -26,10 +26,10 @@
 
 lemma sorted_merge[simp]:
      "List.sorted (merge xs ys) = (List.sorted xs \<and> List.sorted ys)"
-by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
+by (induct xs ys rule: merge.induct, auto)
 
 lemma distinct_merge[simp]: "\<lbrakk> distinct xs; distinct ys; List.sorted xs; List.sorted ys \<rbrakk> \<Longrightarrow> distinct (merge xs ys)"
-by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
+by (induct xs ys rule: merge.induct, auto)
 
 text \<open>The remove function removes an element from a sorted list\<close>
 
@@ -40,7 +40,7 @@
 
 lemma remove': "sorted xs \<and> distinct xs \<Longrightarrow> sorted (remove a xs) \<and> distinct (remove a xs) \<and> set (remove a xs) = set xs - {a}"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 done
 
 lemma set_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> set (remove a xs) = set xs - {a}"
@@ -61,7 +61,6 @@
 lemma remove_insort_commute: "\<lbrakk> a \<noteq> b; sorted xs \<rbrakk> \<Longrightarrow> remove b (insort a xs) = insort a (remove b xs)"
 apply (induct xs)
 apply auto
-apply (auto simp add: sorted_Cons)
 apply (case_tac xs)
 apply auto
 done
@@ -74,7 +73,7 @@
 lemma remove1_eq_remove:
   "sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> remove1 x xs = remove x xs"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 apply (subgoal_tac "x \<notin> set xs")
 apply (simp add: notinset_remove)
 apply fastforce
@@ -83,7 +82,7 @@
 lemma sorted_remove1:
   "sorted xs \<Longrightarrow> sorted (remove1 x xs)"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 done
 
 subsection \<open>Efficient member function for sorted lists\<close>
@@ -93,6 +92,6 @@
 | "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)"
 
 lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" 
-  by (induct xs) (auto simp add: sorted_Cons)
+  by (induct xs) (auto)
 
 end