src/HOL/Library/RBT_Impl.thy
changeset 64243 aee949f6642d
parent 63680 6e1e8b5abbfa
child 64246 15d1ee6e847b
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -1416,7 +1416,7 @@
     1.4          moreover note feven[unfolded feven_def]
     1.5            (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
     1.6          ultimately have "P (2 * (n div 2)) kvs" by -
     1.7 -        thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute)
     1.8 +        thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
     1.9        next
    1.10          case False note ge0
    1.11          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
    1.12 @@ -1462,7 +1462,7 @@
    1.13          moreover note geven[unfolded geven_def]
    1.14          ultimately have "Q (2 * (n div 2)) kvs" by -
    1.15          thus ?thesis using True 
    1.16 -          by(metis div_mod_equality' minus_nat.diff_0 mult.commute)
    1.17 +          by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
    1.18        next
    1.19          case False note ge0
    1.20          moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp