src/HOL/Data_Structures/AVL_Set.thy
changeset 62526 347150095fd2
parent 61678 b594e9277be3
child 63411 e051eea34990
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Sat Mar 05 23:05:07 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Mar 06 10:33:34 2016 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  lemma inorder_del_root:
     1.6    "inorder (del_root (Node h l a r)) = inorder l @ inorder r"
     1.7 -by(induction "Node h l a r" arbitrary: l a r h rule: del_root.induct)
     1.8 +by(cases "Node h l a r" rule: del_root.cases)
     1.9    (auto simp: inorder_balL inorder_balR inorder_del_maxD split: if_splits prod.splits)
    1.10  
    1.11  theorem inorder_delete: