src/HOL/Data_Structures/RBT_Set.thy
changeset 64242 93c6f0da5c70
parent 63411 e051eea34990
child 64947 f6ad52152040
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Oct 16 09:31:04 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4  next
     1.5    case (2 h t t')
     1.6    with RB_mod obtain n where "2*n + 1 = h" 
     1.7 -    by (metis color.distinct(1) mod_div_equality2 parity) 
     1.8 +    by (metis color.distinct(1) mult_div_mod_eq parity) 
     1.9    with 2 balB_h RB_h show ?case by auto
    1.10  next
    1.11    case (3 h t t')