--- a/src/HOL/ex/Groebner_Examples.thy Thu May 06 23:11:58 2010 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy Thu May 06 23:37:07 2010 +0200
@@ -19,7 +19,7 @@
lemma
fixes x :: int
- shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x² + (80 * x + 32))))"
+ shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))"
apply (tactic {* ALLGOALS (CONVERSION
(Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
by (rule refl)