| changeset 71819 | eeff463c49e8 |
| parent 71818 | 986d5abbe77c |
| child 71820 | dd5b8072ca90 |
--- 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>