src/HOL/Enum.thy
changeset 63950 cdc1e59aa513
parent 62390 842917225d56
child 64290 fb5c74a58796
     1.1 --- a/src/HOL/Enum.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -580,7 +580,7 @@
     1.4  instantiation finite_1 :: 
     1.5    "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
     1.6      ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
     1.7 -    one, Divides.div, sgn_if, inverse}"
     1.8 +    one, modulo, sgn_if, inverse}"
     1.9  begin
    1.10  definition [simp]: "Groups.zero = a\<^sub>1"
    1.11  definition [simp]: "Groups.one = a\<^sub>1"
    1.12 @@ -698,7 +698,7 @@
    1.13  instance
    1.14  by intro_classes
    1.15    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.16 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def mod_finite_2_def sgn_finite_2_def
    1.17 +       inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
    1.18       split: finite_2.splits)
    1.19  end
    1.20  
    1.21 @@ -825,7 +825,7 @@
    1.22  instance
    1.23  by intro_classes
    1.24    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    1.25 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def mod_finite_3_def sgn_finite_3_def
    1.26 +       inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
    1.27         less_finite_3_def
    1.28       split: finite_3.splits)
    1.29  end