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