src/HOL/Data_Structures/Tree_Map.thy
changeset 61647 5121b9a57cce
parent 61640 44c9198f210c
child 61651 415e816d3f37
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Thu Nov 12 21:12:09 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Fri Nov 13 12:06:50 2015 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4    "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
     1.5     x # inorder t' = inorder t"
     1.6  by(induction t arbitrary: t' rule: del_min.induct)
     1.7 -  (auto simp: del_list_simps split: prod.splits)
     1.8 +  (auto simp: del_list_simps split: prod.splits if_splits)
     1.9  
    1.10  lemma inorder_delete:
    1.11    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"