# HG changeset patch
# User nipkow
# Date 1553193986 -3600
# Node ID ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc
# Parent  2c48be88f84718fa75d0e09779dba679fcb7a26d# Parent  deb05b4c48bacb832e7f97b0ecb1adefb80fca69
merged

diff -r 2c48be88f847 -r ab8aad4aa76e src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 16:16:43 2019 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Thu Mar 21 19:46:26 2019 +0100
@@ -279,7 +279,7 @@
 "size_fast Leaf = 0" |
 "size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
 
-lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = (if size t = n then 0 else 1)"
+lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
 by(induction t arbitrary: n) auto
 
 lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"