# HG changeset patch
# User haftmann
# Date 1276269242 -7200
# Node ID 61dd8c145da7ff71cd1dfde6cf8427558062bbff
# Parent  982f3e02f3c47fa49e0c571f68a0c53f2ae4eb0a
declare lex_prod_def [code del]

diff -r 982f3e02f3c4 -r 61dd8c145da7 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Jun 11 17:14:01 2010 +0200
+++ b/src/HOL/Wellfounded.thy	Fri Jun 11 17:14:02 2010 +0200
@@ -683,10 +683,8 @@
 text{* Lexicographic combinations *}
 
 definition
- lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
-               (infixr "<*lex*>" 80)
-where
-    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
+  lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+  [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
 
 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
 apply (unfold wf_def lex_prod_def) 
diff -r 982f3e02f3c4 -r 61dd8c145da7 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jun 11 17:14:01 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jun 11 17:14:02 2010 +0200
@@ -26,8 +26,6 @@
   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)"