--- a/src/HOL/Data_Structures/Array_Braun.thy Tue Jan 29 17:33:40 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy Tue Jan 29 13:54:43 2019 +0100
@@ -183,10 +183,10 @@
fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"del_hi n Leaf = Leaf" |
"del_hi n (Node l x r) =
- (if n = 1 then Leaf
- else if even n
- then Node (del_hi (n div 2) l) x r
- else Node l x (del_hi (n div 2) r))"
+ (if n = 1 then Leaf
+ else if even n
+ then Node (del_hi (n div 2) l) x r
+ else Node l x (del_hi (n div 2) r))"
subsubsection "Functional Correctness"