src/HOL/Algebra/UnivPoly.thy
changeset 15076 4b3d280ef06a
parent 15045 d59f7e2e18d3
child 15095 63f5f4c265dd
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Jul 22 19:33:12 2004 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Jul 26 15:48:50 2004 +0200
     1.3 @@ -1162,7 +1162,7 @@
     1.4      next
     1.5        case (Suc j)
     1.6        (* The following could be simplified if there was a reasoner for
     1.7 -        total orders integrated with simip. *)
     1.8 +        total orders integrated with simp. *)
     1.9        have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
    1.10          using Suc by (auto intro!: funcset_mem [OF Rg]) arith
    1.11        have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"