src/HOL/List.thy
changeset 13187 e5434b822a96
parent 13147 491a48cf6023
child 13366 114b7c14084a
     1.1 --- a/src/HOL/List.thy	Thu May 30 10:12:11 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Thu May 30 10:12:52 2002 +0200
     1.3 @@ -531,7 +531,6 @@
     1.4   apply simp_all
     1.5  apply(erule ssubst)
     1.6  apply auto
     1.7 -apply arith
     1.8  done
     1.9  
    1.10  lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"