# HG changeset patch
# User haftmann
# Date 1276350470 -7200
# Node ID f51ff37811bfabd9b96dd95cef1ccd295dfb9113
# Parent  61dd8c145da7ff71cd1dfde6cf8427558062bbff
declare lexn.simps [code del]

diff -r 61dd8c145da7 -r f51ff37811bf src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 11 17:14:02 2010 +0200
+++ b/src/HOL/List.thy	Sat Jun 12 15:47:50 2010 +0200
@@ -4188,8 +4188,8 @@
         
 primrec -- {*The lexicographic ordering for lists of the specified length*}
   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
-    "lexn r 0 = {}"
-  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+    [code del]: "lexn r 0 = {}"
+  | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
 
 definition