--- a/src/HOL/Nat.thy Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/Nat.thy Sun May 06 21:50:17 2007 +0200
@@ -64,7 +64,7 @@
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 *}
@@ -1100,6 +1100,11 @@
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