--- a/src/HOL/Data_Structures/AA_Set.thy Sun Jan 07 21:32:21 2018 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Sun Jan 07 22:15:54 2018 +0100
@@ -29,7 +29,7 @@
fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
"split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
- (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
+ (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
"split t = t"