src/HOL/Library/Multiset.thy
changeset 11655 923e4d0d36d5
parent 11549 e7265e70fd7c
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -749,7 +749,7 @@
     1.4    apply (blast intro: mult_less_trans)
     1.5    done
     1.6  
     1.7 -theorem mult_less_le: "M < N = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
     1.8 +theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
     1.9    apply (unfold le_multiset_def)
    1.10    apply auto
    1.11    done