--- 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)