diff -r b8d7b623e274 -r 1a884605a08b src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Tue May 19 09:33:16 2020 +0200
@@ -86,11 +86,14 @@
      LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
      GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
 
+
+subsection \<open>Proofs\<close>
+
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
 lemmas splits = if_splits tree.splits bal.splits
 
-subsection \<open>Proofs\<close>
+declare Let_def [simp]
 
 subsubsection "Proofs about insertion"
 
@@ -112,7 +115,7 @@
 theorem inorder_insert:
   "\<lbrakk> avl t;  sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
 apply(induction t)
-apply (auto simp: ins_list_simps Let_def split!: splits)
+apply (auto simp: ins_list_simps split!: splits)
 done
 
 
@@ -143,7 +146,7 @@
   avl (delete x t) \<and>
   height t = height (delete x t) + (if decr t (delete x t) then 1 else 0)"
 apply(induction x t rule: delete.induct)
- apply(auto simp: max_absorb1 max_absorb2 Let_def height_1_iff dest: avl_split_max split!: splits prod.splits)
+ apply(auto simp: max_absorb1 max_absorb2 height_1_iff dest: avl_split_max split!: splits prod.splits)
 done
 
 lemma inorder_split_maxD:
@@ -163,7 +166,7 @@
 theorem inorder_delete:
   "\<lbrakk> avl t; sorted(inorder t) \<rbrakk>  \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
 apply(induction t rule: tree2_induct)
-apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD Let_def
+apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD
                  split_max_Leaf neq_Leaf_if_height_neq_0
            simp del: balL.simps balR.simps split!: splits prod.splits)
 done