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.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
```