tuned;
authorwenzelm
Wed Oct 31 15:50:45 2018 +0100 (6 months ago)
changeset 69215ab94035ba6ea
parent 69214 74455459973d
child 69216 1a52baa70aed
tuned;
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Oct 31 14:47:59 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Oct 31 15:50:45 2018 +0100
     1.3 @@ -919,11 +919,11 @@
     1.4            (K (simp_tac (put_simpset ss ctxt) 1));
     1.5        in SOME (thm RS @{thm neq_if_length_neq}) end
     1.6    in
     1.7 -    if m < n andalso submultiset (aconv) (ls,rs) orelse
     1.8 -       n < m andalso submultiset (aconv) (rs,ls)
     1.9 +    if m < n andalso submultiset (op aconv) (ls,rs) orelse
    1.10 +       n < m andalso submultiset (op aconv) (rs,ls)
    1.11      then prove_neq() else NONE
    1.12    end;
    1.13 -in K list_neq end;
    1.14 +in K list_neq end
    1.15  \<close>
    1.16  
    1.17  
    1.18 @@ -1074,7 +1074,7 @@
    1.19          else if lastl aconv lastr then rearr @{thm append_same_eq}
    1.20          else NONE
    1.21        end;
    1.22 -  in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end;
    1.23 +  in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end
    1.24  \<close>
    1.25  
    1.26