--- 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"