src/HOL/Tools/int_arith.ML
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Feb 19 14:47:01 2010 +0100
     1.3 @@ -49,12 +49,12 @@
     1.4    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
     1.5    proc = proc1, identifier = []};
     1.6  
     1.7 -fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
     1.8 -  | check (Const (@{const_name Algebras.one}, _)) = true
     1.9 +fun check (Const (@{const_name Groups.one}, @{typ int})) = false
    1.10 +  | check (Const (@{const_name Groups.one}, _)) = true
    1.11    | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    1.12 -      @{const_name Algebras.times}, @{const_name Algebras.uminus},
    1.13 -      @{const_name Algebras.minus}, @{const_name Algebras.plus},
    1.14 -      @{const_name Algebras.zero},
    1.15 +      @{const_name Groups.times}, @{const_name Groups.uminus},
    1.16 +      @{const_name Groups.minus}, @{const_name Groups.plus},
    1.17 +      @{const_name Groups.zero},
    1.18        @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    1.19    | check (a $ b) = check a andalso check b
    1.20    | check _ = false;