# HG changeset patch
# User nipkow
# Date 1447427850 -3600
# Node ID 415e816d3f37fe3f5a65a9836d873b0e2b691a2b
# Parent  2be10c63a0ab7792a2aea0de6eeac0290d589fd1
unnecessary precondition

diff -r 2be10c63a0ab -r 415e816d3f37 src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Fri Nov 13 12:43:54 2015 +0000
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Fri Nov 13 16:17:30 2015 +0100
@@ -34,18 +34,10 @@
   "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
 by (induction t) (auto simp: map_of_simps split: option.split)
 
-
 lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
 by(induction t) (auto simp: upd_list_simps)
 
-
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
-   x # inorder t' = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
-  (auto simp: del_list_simps split: prod.splits if_splits)
-
 lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
diff -r 2be10c63a0ab -r 415e816d3f37 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Nov 13 12:43:54 2015 +0000
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Fri Nov 13 16:17:30 2015 +0100
@@ -50,8 +50,7 @@
 
 
 lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
-   x # inorder t' = inorder t"
+  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
 by(induction t arbitrary: t' rule: del_min.induct)
   (auto simp: sorted_lems split: prod.splits if_splits)