src/HOL/Nat.thy
changeset 55534 b18bdcbda41b
parent 55469 b19dd108f0c2
child 55575 a5e33e18fb5c
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4  instantiation nat :: comm_monoid_diff
     1.5  begin
     1.6  
     1.7 -primrec plus_nat where
     1.8 +old_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 -primrec minus_nat where
    1.17 +old_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 -primrec times_nat where
    1.26 +old_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 -primrec less_eq_nat where
    1.35 +old_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 -primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.44 +old_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"
    1.50    by (induct m) (simp_all add: add_ac distrib_right)
    1.51  
    1.52 -primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.53 +old_primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.54    "of_nat_aux inc 0 i = i"
    1.55  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    1.56