summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/UnivPoly.thy

changeset 15076 | 4b3d280ef06a |

parent 15045 | d59f7e2e18d3 |

child 15095 | 63f5f4c265dd |

--- a/src/HOL/Algebra/UnivPoly.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Mon Jul 26 15:48:50 2004 +0200 @@ -1162,7 +1162,7 @@ next case (Suc j) (* The following could be simplified if there was a reasoner for - total orders integrated with simip. *) + total orders integrated with simp. *) have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R" using Suc by (auto intro!: funcset_mem [OF Rg]) arith have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"