# HG changeset patch
# User nipkow
# Date 1588765921 -7200
# Node ID eeff463c49e8850c18ef6d2bdce81b76f5ae549a
# Parent  986d5abbe77c188a4534c8f7c6b44d50916a9602
tuned

diff -r 986d5abbe77c -r eeff463c49e8 src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Wed May 06 10:46:19 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Wed May 06 13:52:01 2020 +0200
@@ -110,7 +110,7 @@
 
 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
 
-lemmas splits = if_splits tree.splits tree.splits tree_bal2.splits bal.splits
+lemmas splits = if_splits tree.splits tree_bal2.splits bal.splits
 
 subsection \<open>Proofs\<close>