# HG changeset patch
# User nipkow
# Date 1447266138 -3600
# Node ID 40ca618e1b2d349b7b9433d7677e08ee819ee5e6
# Parent  34460a266346e76a317df781c8a8cfcd3e34f235
tuned

diff -r 34460a266346 -r 40ca618e1b2d src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Nov 11 18:32:36 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Nov 11 19:22:18 2015 +0100
@@ -68,7 +68,7 @@
 
 lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
   ins_list x (xs @ a # ys) =
-  (if a \<le> x then xs @ ins_list x (a#ys) else ins_list x xs @ (a#ys))"
+  (if x < a then ins_list x xs @ (a#ys) else xs @ ins_list x (a#ys))"
 by(induction xs) (auto simp: sorted_lems)
 
 text\<open>In principle, @{thm ins_list_sorted} suffices, but the following two
@@ -76,7 +76,7 @@
 
 corollary ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
   ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
-by(simp add: ins_list_sorted)
+by(auto simp add: ins_list_sorted)
 
 corollary ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
   ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"