summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Polynomial_FPS.thy

changeset 64911 | f0e07600de47 |

parent 64272 | f76b6dda2e56 |

child 65366 | 10ca63a18e56 |

1.1 --- a/src/HOL/Library/Polynomial_FPS.thy Tue Jan 17 11:26:21 2017 +0100 1.2 +++ b/src/HOL/Library/Polynomial_FPS.thy Tue Jan 17 13:59:10 2017 +0100 1.3 @@ -163,7 +163,7 @@ 1.4 The following simproc can reduce the equality of two polynomial FPSs two equality of the 1.5 respective polynomials. A polynomial FPS is one that only has finitely many non-zero 1.6 coefficients and can therefore be written as @{term "fps_of_poly p"} for some 1.7 - polynomial @{text "p"}. 1.8 + polynomial \<open>p\<close>. 1.9 1.10 This may sound trivial, but it covers a number of annoying side conditions like 1.11 @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.