src/HOL/Data_Structures/AVL_Bal_Set.thy

--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -139,7 +139,6 @@
    avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
 apply(induction t arbitrary: t' a rule: split_max_induct)
  apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
-apply(fastforce)+
 done
 
 lemma avl_delete: "avl t \<Longrightarrow>