# HG changeset patch
# User berghofe
# Date 1007994199 -3600
# Node ID fb5851b71a82f51c9a765a0342f56df0ef5c4cd6
# Parent  e90a4f5a27f017b34b7b77d1add3dfb2ea6d5840
Added code generator setup.

diff -r e90a4f5a27f0 -r fb5851b71a82 src/HOL/Integ/NatBin.thy
--- 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