# HG changeset patch
# User wenzelm
# Date 1461160919 -7200
# Node ID b1549a05f44dbc89fa616cc8bf4a499bed0c4b73
# Parent  b07c9f5d38027d0b69106e841bec7a7b6c75da71
proper latex;

diff -r b07c9f5d3802 -r b1549a05f44d src/HOL/Library/Polynomial.thy
--- 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"