# HG changeset patch
# User haftmann
# Date 1273181827 -7200
# Node ID 5779d9fbedd0171522efafb6986b876e090178f2
# Parent  b91ef008b5605a1618b2eb31e0450b4fbc6fb222
xsymbolized

diff -r b91ef008b560 -r 5779d9fbedd0 src/HOL/ex/Groebner_Examples.thy
--- 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)