Added code generator setup.

--- a/src/HOL/Integ/NatBin.thy	Mon Dec 10 15:18:57 2001 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Dec 10 15:23:19 2001 +0100
@@ -20,4 +20,23 @@
 
 use "nat_bin.ML"	setup nat_bin_arith_setup
 
+
+subsection {* Configuration of the code generator *}
+
+types_code
+  "int" ("int")
+
+lemmas [code] = int_0 int_Suc
+
+lemma [code]: "nat x = (if x <= 0 then 0 else Suc (nat (x - 1)))"
+  by (simp add: Suc_nat_eq_nat_zadd1)
+
+consts_code
+  "0" :: "int"                  ("0")
+  "1" :: "int"                  ("1")
+  "uminus" :: "int => int"      ("~")
+  "op +" :: "int => int => int" ("(_ +/ _)")
+  "op *" :: "int => int => int" ("(_ */ _)")
+  "neg"                         ("(_ < 0)")
+
 end