src/HOL/Divides.thy
changeset 58410 6d46ad54a2ab
parent 57514 bdc2c6b40bf2
child 58511 97aec08d6f28
     1.1 --- a/src/HOL/Divides.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -1664,7 +1664,7 @@
     1.4  lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
     1.5  by (subst posDivAlg.simps, auto)
     1.6  
     1.7 -lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
     1.8 +lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
     1.9  by (subst negDivAlg.simps, auto)
    1.10  
    1.11  lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"