src/HOL/Wellfounded.thy

 apply (rule wf_less_than [THEN wf_inv_image])
 done
 
 text{* Lexicographic combinations *}
 
-definition
-  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}"
+definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+  "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) 
 apply (rule allI, rule impI)
 apply (simp (no_asm_use) only: split_paired_All)

  "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
   (A \<union> C, B \<union> D) \<in> max_ext R"
 by (force elim!: max_ext.cases)
 
 
-definition
-  min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
-where
-  [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
+definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"  where
+  "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
 
 lemma min_ext_wf:
   assumes "wf r"
   shows "wf (min_ext r)"
 proof (rule wfI_min)