| changeset 61428 | 5e1938107371 |
| parent 61232 | c46faf9762f7 |
| child 61581 | 00d9682e8dd7 |
--- a/src/HOL/Data_Structures/AVL_Set.thy Tue Oct 13 14:49:15 2015 +0100 +++ b/src/HOL/Data_Structures/AVL_Set.thy Tue Oct 13 17:06:37 2015 +0200 @@ -130,9 +130,7 @@ case 3 thus ?case by(simp add: inorder_insert) next case 4 thus ?case by(simp add: inorder_delete) -next - case 5 thus ?case .. -qed +qed (rule TrueI)+ subsection {* AVL invariants *}