src/HOL/Library/Multiset.thy
changeset 13596 ee5f79b210c1
parent 12399 2ba27248af7f
child 13601 fd3e3d6b37b2
--- a/src/HOL/Library/Multiset.thy	Fri Sep 27 16:44:50 2002 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 15:44:21 2002 +0200
@@ -691,7 +691,7 @@
 
 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   apply (insert mult_less_not_refl)
-  apply blast
+  apply fast
   done