# HG changeset patch
# User traytel
# Date 1390285085 -3600
# Node ID f05b42b908f426be0f1a648bc1fdcd0a86ca1ee5
# Parent  c43394c2e5eca9c1881e9e813588c7f2556ea974
compile

diff -r c43394c2e5ec -r f05b42b908f4 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Tue Jan 21 01:14:49 2014 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy	Tue Jan 21 07:18:05 2014 +0100
@@ -12,7 +12,7 @@
 
 lemma
   fixes x :: int
-  shows "x ^ 3 = x ^ 3" 
+  shows "x ^ 3 = x ^ 3"
   apply (tactic {* ALLGOALS (CONVERSION
     (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
   by (rule refl)
@@ -45,10 +45,11 @@
 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 + a*e\<^sup>2*c + f*d*b\<^sup>2 = 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 +
+    a * e\<^sup>2 * c + f * d * b\<^sup>2 = 0"
   using assms by algebra
 
 lemma "(x::int)^3  - x^2  - 5*x - 3 = 0 \<longleftrightarrow> (x = 3 \<or> x = -1)"