src/HOL/Data_Structures/AA_Set.thy
changeset 67369 7360fe6bb423
parent 67040 c1b87d15774a
child 67406 23307fd33906
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 21:32:21 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 22:15:54 2018 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
     1.6  "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
     1.7 -   (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
     1.8 +   (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
     1.9      then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
    1.10      else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
    1.11  "split t = t"