src/HOL/Code_Numeral.thy
changeset 60352 d46de31a50c4
parent 59816 034b13f4efae
child 60562 24af00b010cf
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -150,11 +150,11 @@
     1.4  instantiation integer :: "{ring_div, equal, linordered_idom}"
     1.5  begin
     1.6  
     1.7 -lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
     1.8 -  is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
     1.9 +lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.10 +  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.11    .
    1.12  
    1.13 -declare div_integer.rep_eq [simp]
    1.14 +declare divide_integer.rep_eq [simp]
    1.15  
    1.16  lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.17    is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
    1.18 @@ -709,11 +709,11 @@
    1.19  instantiation natural :: "{semiring_div, equal, linordered_semiring}"
    1.20  begin
    1.21  
    1.22 -lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    1.23 -  is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.24 +lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    1.25 +  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.26    .
    1.27  
    1.28 -declare div_natural.rep_eq [simp]
    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"