src/HOL/Data_Structures/AA_Set.thy
changeset 63636 6f38b7abb648
parent 63411 e051eea34990
child 67040 c1b87d15774a
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sun Aug 07 12:10:49 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Tue Aug 09 17:00:36 2016 +0200
     1.3 @@ -329,7 +329,7 @@
     1.4    from lDown_tDouble and r obtain rrlv rrr rra rrl where
     1.5      rr :"rr = Node rrlv rrr rra rrl" by (cases rr) auto
     1.6    from  lDown_tDouble show ?thesis unfolding adjust_def r rr
     1.7 -    apply (cases rl) apply (auto simp add: invar.simps(2))
     1.8 +    apply (cases rl) apply (auto simp add: invar.simps(2) split!: if_split)
     1.9      using lDown_tDouble by (auto simp: split_case lvl_0_iff  elim:lvl.elims split: tree.split)
    1.10  qed (auto simp: split_case invar.simps(2) adjust_def split: tree.splits)
    1.11