| changeset 22744 | 5cbe966d67a2 |
| parent 22718 | 936f7580937d |
| child 22845 | 5f9138bcb3d7 |
--- a/src/HOL/Nat.thy Fri Apr 20 11:21:41 2007 +0200 +++ b/src/HOL/Nat.thy Fri Apr 20 11:21:42 2007 +0200 @@ -62,7 +62,9 @@ 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)" .. + le_def: "m \<le> (n::nat) == ~ (n < m)" .. + +lemmas [code nofunc] = less_def le_def text {* Induction *}