author | wenzelm |
Sun, 03 Jun 2007 23:16:42 +0200 | |
changeset 23214 | dc23c062b58c |
parent 23213 | 43553703267c |
child 23215 | 20b5558a5419 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/List.thy Sun Jun 03 23:16:41 2007 +0200 +++ b/src/HOL/List.thy Sun Jun 03 23:16:42 2007 +0200 @@ -381,8 +381,8 @@ (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1)); in SOME (thm RS @{thm neq_if_length_neq}) end in - if m < n andalso gen_submultiset (op aconv) (ls,rs) orelse - n < m andalso gen_submultiset (op aconv) (rs,ls) + if m < n andalso submultiset (op aconv) (ls,rs) orelse + n < m andalso submultiset (op aconv) (rs,ls) then prove_neq() else NONE end;