src/HOL/Data_Structures/AA_Set.thy
changeset 67613 ce654b0e6d69
parent 67406 23307fd33906
child 67967 5a4280946a25
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4  
     1.5  
     1.6  lemma lvl_insert_incr_iff: "(lvl(insert a t) = lvl t + 1) \<longleftrightarrow>
     1.7 -  (EX l x r. insert a t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
     1.8 +  (\<exists>l x r. insert a t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)"
     1.9  apply(cases t)
    1.10  apply(auto simp add: skew_case split_case split: if_splits)
    1.11  apply(auto split: tree.splits if_splits)