src/HOL/Nat.thy

   Zero_nat_def: "0 == Abs_Nat Zero_Rep"
   One_nat_def [simp]: "1 == Suc 0"
   less_def: "m < n == (m, n) : pred_nat^+"
   le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
 
-lemmas [code nofunc] = less_def le_def
+lemmas [code func del] = less_def le_def
 
 text {* Induction *}
 
 lemma Rep_Nat': "Nat (Rep_Nat x)"
   by (rule Rep_Nat [simplified mem_Collect_eq])

     "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   using Suc_le_eq less_Suc_eq_le by simp_all
 
 
 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
+
+lemma subst_equals:
+  assumes 1: "t = s" and 2: "u = t"
+  shows "u = s"
+  using 2 1 by (rule trans)
 
 use "arith_data.ML"
 setup arith_setup
 
 text{*The following proofs may rely on the arithmetic proof procedures.*}