# HG changeset patch
# User nipkow
# Date 1446817385 -3600
# Node ID d07d0d5a572b27dc1a7cf99bf008874bacf8e8bd
# Parent  1d2907d0ed73dff4718af177572b959ee8e48c6b
tuned

diff -r 1d2907d0ed73 -r d07d0d5a572b src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Nov 05 18:38:08 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Fri Nov 06 14:43:05 2015 +0100
@@ -55,7 +55,7 @@
 "ins_list x (a#xs) =
   (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
 
-lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
+lemma set_ins_list: "elems (ins_list x xs) = insert x (elems xs)"
 by(induction xs) auto
 
 lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
@@ -86,7 +86,7 @@
 lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
 by (induct xs) simp_all
 
-lemma elems_del_list_eq [simp]:
+lemma elems_del_list_eq:
   "distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
 apply(induct xs)
  apply simp
diff -r 1d2907d0ed73 -r d07d0d5a572b src/HOL/Data_Structures/Set_by_Ordered.thy
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Thu Nov 05 18:38:08 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Fri Nov 06 14:43:05 2015 +0100
@@ -47,10 +47,10 @@
 next
   case 2 thus ?case by(simp add: isin)
 next
-  case 3 thus ?case by(simp add: insert)
+  case 3 thus ?case by(simp add: insert set_ins_list)
 next
-  case (4 s x) show ?case
-    using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
+  case (4 s x) thus ?case
+    using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
 next
   case 5 thus ?case by(simp add: empty inv_empty)
 next