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})"