diff -r 0bfdbbe657eb -r 50aaae6ae4db src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Aug 08 08:19:39 2006 +0200
+++ b/src/HOL/Nat.thy	Tue Aug 08 08:19:44 2006 +0200
@@ -1043,6 +1043,10 @@
 
 subsection {* Code generator setup *}
 
+lemma one_is_suc_zero [code inline]:
+  "1 = Suc 0"
+  by simp
+
 code_alias
   "nat" "Nat.nat"
   "0" "Nat.Zero"