name shifts
authorhaftmann
Wed Sep 20 12:24:11 2006 +0200 (2006-09-20)
changeset 2064005e6042394b9
parent 20639 3aa960295c54
child 20641 12554634e552
name shifts
src/HOL/Divides.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Sep 20 12:23:54 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Sep 20 12:24:11 2006 +0200
     1.3 @@ -896,6 +896,11 @@
     1.4    "m mod n = snd (divmod m n)"
     1.5    unfolding divmod_def by simp
     1.6  
     1.7 +code_constname
     1.8 +  "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat"
     1.9 +  "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat"
    1.10 +  Divides.divmod "IntDef.divmod_nat"
    1.11 +
    1.12  hide (open) const divmod
    1.13  
    1.14  
     2.1 --- a/src/HOL/Nat.thy	Wed Sep 20 12:23:54 2006 +0200
     2.2 +++ b/src/HOL/Nat.thy	Wed Sep 20 12:24:11 2006 +0200
     2.3 @@ -1062,4 +1062,18 @@
     2.4  lemma [code func]:
     2.5    "OperationalEquality.eq 0 (Suc m) = False" unfolding eq_def by auto
     2.6  
     2.7 +code_typename
     2.8 +  "nat" "IntDef.nat"
     2.9 +
    2.10 +code_constname
    2.11 +  "0 \<Colon> nat" "IntDef.zero_nat"
    2.12 +  "1 \<Colon> nat" "IntDef.one_nat"
    2.13 +  Suc "IntDef.succ_nat"
    2.14 +  "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.plus_nat"
    2.15 +  "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.minus_nat"
    2.16 +  "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.times_nat"
    2.17 +  "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_nat"
    2.18 +  "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_eq_nat"
    2.19 +  "OperationalEquality.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.eq_nat"
    2.20 +
    2.21  end