src/HOL/Computational_Algebra/Polynomial.thy
changeset 67369 7360fe6bb423
parent 67091 1393c2340eec
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 21:32:21 2018 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 22:15:54 2018 +0100
     1.3 @@ -2893,7 +2893,7 @@
     1.4    where
     1.5      "divide_poly_main lc q r d dr (Suc n) =
     1.6        (let cr = coeff r dr; a = cr div lc; mon = monom a n in
     1.7 -        if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
     1.8 +        if False \<or> a * lc = cr then \<comment> \<open>\<open>False \<or>\<close> is only because of problem in function-package\<close>
     1.9            divide_poly_main
    1.10              lc
    1.11              (q + mon)