Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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"
isabelle