changeset 62175 | 8ffc4d0e652d |
parent 62128 | 3201ddb00097 |
--- a/src/HOL/Library/Poly_Deriv.thy Wed Jan 13 23:02:28 2016 +0100 +++ b/src/HOL/Library/Poly_Deriv.thy Wed Jan 13 23:07:06 2016 +0100 @@ -183,7 +183,7 @@ { fix b assume "b \<in> as" - hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto + hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})" unfolding id2 by (subst setprod.insert, insert insert, auto)