src/HOL/Nat.thy
 changeset 55575 a5e33e18fb5c parent 55534 b18bdcbda41b child 55642 63beb38e9258
```     1.1 --- a/src/HOL/Nat.thy	Wed Feb 19 08:34:32 2014 +0100
1.2 +++ b/src/HOL/Nat.thy	Wed Feb 19 08:34:33 2014 +0100
1.3 @@ -187,7 +187,7 @@
1.4  instantiation nat :: comm_monoid_diff
1.5  begin
1.6
1.7 -old_primrec plus_nat where
1.8 +primrec plus_nat where
1.9    add_0:      "0 + n = (n\<Colon>nat)"
1.10  | add_Suc:  "Suc m + n = Suc (m + n)"
1.11
1.12 @@ -202,7 +202,7 @@
1.13  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
1.14    by simp
1.15
1.16 -old_primrec minus_nat where
1.17 +primrec minus_nat where
1.18    diff_0 [code]: "m - 0 = (m\<Colon>nat)"
1.19  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
1.20
1.21 @@ -235,7 +235,7 @@
1.22  definition
1.23    One_nat_def [simp]: "1 = Suc 0"
1.24
1.25 -old_primrec times_nat where
1.26 +primrec times_nat where
1.27    mult_0:     "0 * n = (0\<Colon>nat)"
1.28  | mult_Suc: "Suc m * n = n + (m * n)"
1.29
1.30 @@ -414,7 +414,7 @@
1.31  instantiation nat :: linorder
1.32  begin
1.33
1.34 -old_primrec less_eq_nat where
1.35 +primrec less_eq_nat where
1.36    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
1.37  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
1.38
1.39 @@ -1303,7 +1303,7 @@
1.40    funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
1.41  begin
1.42
1.43 -old_primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.44 +primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.45    "funpow 0 f = id"
1.46  | "funpow (Suc n) f = f o funpow n f"
1.47
1.48 @@ -1410,7 +1410,7 @@
1.49  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"