# HG changeset patch
# User wenzelm
# Date 1390407728 -3600
# Node ID fbf24a326206cf27486bc9851577f3b59c38fd73
# Parent  0ee5c17f22073459d75477f6f113f63d758c2291
removed junk;

diff -r 0ee5c17f2207 -r fbf24a326206 src/HOL/ex/Groebner_Examples.thy
--- 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 +