src/HOL/ex/Groebner_Examples.thy
 changeset 36753 5cf4e9128f22 parent 36724 5779d9fbedd0 child 42463 f270e3e18be5
```     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri May 07 16:12:25 2010 +0200
1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Fri May 07 16:12:26 2010 +0200
1.3 @@ -14,21 +14,21 @@
1.4    fixes x :: int
1.5    shows "x ^ 3 = x ^ 3"
1.6    apply (tactic {* ALLGOALS (CONVERSION
1.7 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.8 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
1.9    by (rule refl)
1.10
1.11  lemma
1.12    fixes x :: int
1.13    shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\<twosuperior> + (80 * x + 32))))"
1.14    apply (tactic {* ALLGOALS (CONVERSION
1.15 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.16 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
1.17    by (rule refl)
1.18
1.19  schematic_lemma
1.20    fixes x :: int
1.21    shows "(x - (-2))^5  * (y - 78) ^ 8 = ?X"
1.22    apply (tactic {* ALLGOALS (CONVERSION
1.23 -    (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *})
1.24 +    (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
1.25    by (rule refl)
1.26
1.27  lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
```