Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Multiset.thy
changeset 14445 4392cb82018b
parent 13601 fd3e3d6b37b2
child 14691 e1eedc8cad37 
--- a/src/HOL/Library/Multiset.thy	Mon Mar 08 12:16:57 2004 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 08 12:17:43 2004 +0100
@@ -801,7 +801,6 @@
     apply (rule one_step_implies_mult)
       apply (simp only: trans_def)
       apply auto
-  apply (blast intro: order_less_trans)
   done
 
 theorem union_upper1: "A <= A + (B::'a::order multiset)"
isabelle