# 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 \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.\
+ \div_field_poly_impl\ is a bit more efficient than the generic polynomial division.\
lemma div_field_poly_impl[code_unfold]: "op div = div_field_poly_impl"
proof (intro ext)
fix f g :: "'a poly"