src/HOL/Nat.thy

   apply (rule nat_less_cases, erule_tac [2] _)
   apply (fastsimp elim!: less_SucE)
   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