src/HOL/Decision_Procs/commutative_ring_tac.ML
changeset 34974 18b41bba42b5
parent 33495 1464ddca182b
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4  struct
     1.5  
     1.6  (* Zero and One of the commutative ring *)
     1.7 -fun cring_zero T = Const (@{const_name HOL.zero}, T);
     1.8 -fun cring_one T = Const (@{const_name HOL.one}, T);
     1.9 +fun cring_zero T = Const (@{const_name Algebras.zero}, T);
    1.10 +fun cring_one T = Const (@{const_name Algebras.one}, T);
    1.11  
    1.12  (* reification functions *)
    1.13  (* add two polynom expressions *)
    1.14 @@ -49,13 +49,13 @@
    1.15    | reif_pol T vs t = pol_Pc T $ t;
    1.16  
    1.17  (* reification of polynom expressions *)
    1.18 -fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
    1.19 +fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) =
    1.20        polex_add T $ reif_polex T vs a $ reif_polex T vs b
    1.21 -  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
    1.22 +  | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
    1.23        polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    1.24 -  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
    1.25 +  | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
    1.26        polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    1.27 -  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
    1.28 +  | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
    1.29        polex_neg T $ reif_polex T vs a
    1.30    | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
    1.31        polex_pow T $ reif_polex T vs a $ n