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 11655 923e4d0d36d5
parent 11549 e7265e70fd7c
child 11701 3d51fbf81c17 
--- a/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:16 2001 +0200
@@ -749,7 +749,7 @@
   apply (blast intro: mult_less_trans)
   done
 
-theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
+theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   apply (unfold le_multiset_def)
   apply auto
   done
isabelle