# HG changeset patch
# User haftmann
# Date 1196957144 -3600
# Node ID cab4f808f791c088bb21c95dbcd199ac50a1882c
# Parent  f0fc8531c9097fb7f015eccf1c092e394e0b2ae1
temporary code generator work arounds

diff -r f0fc8531c909 -r cab4f808f791 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 06 16:56:00 2007 +0100
+++ b/src/HOL/List.thy	Thu Dec 06 17:05:44 2007 +0100
@@ -109,6 +109,7 @@
 where
   append_Nil:"[] @ ys = ys"
   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
+declare append.simps [code]
 
 primrec
   "rev([]) = []"
@@ -3177,6 +3178,7 @@
 where 
   "x mem [] \<longleftrightarrow> False"
   | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
+declare member.simps [code]
 
 primrec
   "null [] = True"
diff -r f0fc8531c909 -r cab4f808f791 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Dec 06 16:56:00 2007 +0100
+++ b/src/HOL/Nat.thy	Thu Dec 06 17:05:44 2007 +0100
@@ -1162,6 +1162,7 @@
 where
   of_nat_0:     "of_nat 0 = 0"
   | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+declare of_nat.simps [code]
 
 lemma of_nat_1 [simp]: "of_nat 1 = 1"
   by simp