summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"