# HG changeset patch
# User haftmann
# Date 1276165514 -7200
# Node ID b39f640b94d44e8a78aeccee5431b92707ecbf98
# Parent  476270a6c2dce0866b4cb3f6e5cac7f1450deceb
tailored set of code equations manually

diff -r 476270a6c2dc -r b39f640b94d4 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Thu Jun 10 12:24:03 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Thu Jun 10 12:25:14 2010 +0200
@@ -26,6 +26,8 @@
   While_Combinator
 begin
 
+declare lexn.simps [code del]
+
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     empty: "sublist [] xs"
   | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"