src/HOL/List.thy
changeset 68646 7dc9fe795dae
parent 68527 2f4e2aab190a
child 68709 6d9eca4805ff
     1.1 --- a/src/HOL/List.thy	Mon Jul 16 23:33:38 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jul 17 22:18:27 2018 +0100
     1.3 @@ -5804,14 +5804,11 @@
     1.4  by (induct n arbitrary: xs ys) auto
     1.5  
     1.6  lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
     1.7 -apply (unfold lex_def)
     1.8 -apply (rule wf_UN)
     1.9 -apply (blast intro: wf_lexn, clarify)
    1.10 -apply (rename_tac m n)
    1.11 -apply (subgoal_tac "m \<noteq> n")
    1.12 - prefer 2 apply blast
    1.13 -apply (blast dest: lexn_length not_sym)
    1.14 -done
    1.15 +  apply (unfold lex_def)
    1.16 +  apply (rule wf_UN)
    1.17 +   apply (simp add: wf_lexn)
    1.18 +  apply (metis DomainE Int_emptyI RangeE lexn_length)
    1.19 +  done
    1.20  
    1.21  lemma lexn_conv:
    1.22    "lexn r n =