src/HOL/Code_Numeral.thy
changeset 63950 cdc1e59aa513
parent 63174 57c0d60e491c
child 64178 12e6c3bbb488
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -175,11 +175,11 @@
     1.4  
     1.5  declare divide_integer.rep_eq [simp]
     1.6  
     1.7 -lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
     1.8 -  is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
     1.9 +lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.10 +  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.11    .
    1.12  
    1.13 -declare mod_integer.rep_eq [simp]
    1.14 +declare modulo_integer.rep_eq [simp]
    1.15  
    1.16  lift_definition abs_integer :: "integer \<Rightarrow> integer"
    1.17    is "abs :: int \<Rightarrow> int"
    1.18 @@ -534,7 +534,7 @@
    1.19    moreover have "2 * (j div 2) = j - j mod 2"
    1.20      by (simp add: zmult_div_cancel mult.commute)
    1.21    ultimately show ?thesis
    1.22 -    by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le
    1.23 +    by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
    1.24        nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    1.25        (auto simp add: mult_2 [symmetric])
    1.26  qed
    1.27 @@ -761,11 +761,11 @@
    1.28  
    1.29  declare divide_natural.rep_eq [simp]
    1.30  
    1.31 -lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    1.32 -  is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.33 +lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    1.34 +  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.35    .
    1.36  
    1.37 -declare mod_natural.rep_eq [simp]
    1.38 +declare modulo_natural.rep_eq [simp]
    1.39  
    1.40  lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
    1.41    is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.42 @@ -973,7 +973,7 @@
    1.43    functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
    1.44      "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
    1.45      "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
    1.46 -    "Divides.mod :: natural \<Rightarrow> _"
    1.47 +    "modulo :: natural \<Rightarrow> _"
    1.48      integer_of_natural natural_of_integer
    1.49  
    1.50  end