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

src/HOL/Library/Polynomial.thy

changeset 63034 | b1549a05f44d |

parent 63027 | 8de0ebee3f1c |

child 63035 | 6c018eb1e177 |

--- a/src/HOL/Library/Polynomial.thy Wed Apr 20 14:09:08 2016 +0200 +++ b/src/HOL/Library/Polynomial.thy Wed Apr 20 16:01:59 2016 +0200 @@ -2518,7 +2518,7 @@ text \<open>We do not declare the following lemma as code equation, since then polynomial division on non-fields will no longer be executable. However, a code-unfold is possible, since - div_field_poly_impl is a bit more efficient than the generic polynomial division.\<close> + \<open>div_field_poly_impl\<close> is a bit more efficient than the generic polynomial division.\<close> lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl" proof (intro ext) fix f g :: "'a poly"