--- a/src/HOL/Nat.thy Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Nat.thy Tue Jan 17 16:36:57 2006 +0100
@@ -1023,5 +1023,12 @@
apply (fastsimp dest: mult_less_mono2)
done
+subsection {* Code generator setup *}
+
+code_alias
+ "nat" "Nat.nat"
+ "0" "Nat.Zero"
+ "1" "Nat.One"
+ "Suc" "Nat.Suc"
end