changeset 19623 | 12e6cc4382ae |
parent 19607 | 07eeb832f28d |
child 19770 | be5c23ebe1eb |
--- a/src/HOL/List.thy Fri May 12 10:38:00 2006 +0200 +++ b/src/HOL/List.thy Fri May 12 11:19:41 2006 +0200 @@ -2428,7 +2428,7 @@ lemma lenlex_conv: "lenlex r = {(xs,ys). length xs < length ys | length xs = length ys \<and> (xs, ys) : lex r}" -by (simp add: lenlex_def diag_def lex_prod_def measure_def inv_image_def) +by (simp add: lenlex_def diag_def lex_prod_def inv_image_def) lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r" by (simp add: lex_conv)