# HG changeset patch # User haftmann # Date 1190831277 -7200 # Node ID f5015dd2431b7a3b3238c012490318ac92dfceaf # Parent e2b3a1065676b8f348ac6d8af3d9a605cc39669d added code lemma for 1 diff -r e2b3a1065676 -r f5015dd2431b src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Sep 26 20:27:55 2007 +0200 +++ b/src/HOL/Nat.thy Wed Sep 26 20:27:57 2007 +0200 @@ -69,7 +69,7 @@ less_def: "m < n == (m, n) : pred_nat^+" le_def: "m \ (n::nat) == ~ (n < m)" .. -lemmas [code func del] = Zero_nat_def One_nat_def less_def le_def +lemmas [code func del] = Zero_nat_def less_def le_def text {* Induction *}