author | nipkow |
Sat, 26 Aug 2017 17:52:00 +0200 | |
changeset 66516 | 97c2d3846e10 |
parent 66515 | 85c505c98332 |
child 66517 | 7c7977f6c4ce |
--- a/src/HOL/Data_Structures/Balance.thy Sat Aug 26 16:47:25 2017 +0200 +++ b/src/HOL/Data_Structures/Balance.thy Sat Aug 26 17:52:00 2017 +0200 @@ -7,8 +7,6 @@ "HOL-Library.Tree_Real" begin -(* FIXME rm floor_eq_iff / rename unique \<rightarrow> eq *) - fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where "bal n xs = (if n=0 then (Leaf,xs) else (let m = n div 2;