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.