summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 20 Apr 2016 16:01:59 +0200 | |

changeset 63034 | b1549a05f44d |

parent 63033 | b07c9f5d3802 |

child 63035 | 6c018eb1e177 |

proper latex;

--- 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"