src/HOL/List.thy
changeset 13601 fd3e3d6b37b2
parent 13585 db4005b40cc6
child 13737 e564c3d2d174
     1.1 --- a/src/HOL/List.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -1268,10 +1268,9 @@
     1.4   apply simp
     1.5   apply blast
     1.6  apply (simp add: image_Collect lex_prod_def)
     1.7 -apply auto
     1.8 +apply safe
     1.9  apply blast
    1.10 - apply (rename_tac a xys x xs' y ys')
    1.11 - apply (rule_tac x = "a # xys" in exI)
    1.12 + apply (rule_tac x = "ab # xys" in exI)
    1.13   apply simp
    1.14  apply (case_tac xys)
    1.15   apply simp_all