author | wenzelm |
Wed, 22 Jan 2014 17:22:08 +0100 | |
changeset 55115 | fbf24a326206 |
parent 55114 | 0ee5c17f2207 |
child 55116 | c05328661883 |
--- a/src/HOL/ex/Groebner_Examples.thy Wed Jan 22 17:14:27 2014 +0100 +++ b/src/HOL/ex/Groebner_Examples.thy Wed Jan 22 17:22:08 2014 +0100 @@ -45,7 +45,7 @@ lemma "(4::int) + 0 = 4" apply algebra? by simp -term "op *c" + lemma assumes "a * x\<^sup>2 + b * x + c = (0::int)" and "d * x\<^sup>2 + e * x + f = 0" shows "d\<^sup>2 * c\<^sup>2 - 2 * d * c * a * f + a\<^sup>2 * f\<^sup>2 - e * d * b * c - e * b * a * f +