Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added code lemma for 1
authorhaftmann
Wed, 26 Sep 2007 20:27:57 +0200
changeset 24729 f5015dd2431b
parent 24728 e2b3a1065676
child 24730 a87d8d31abc0
added code lemma for 1
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- 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 \<le> (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 *}
isabelle