equal
deleted
inserted
replaced
1697 lemma mult_less_asym: |
1697 lemma mult_less_asym: |
1698 "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P" |
1698 "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P" |
1699 by (fact multiset_order.less_asym) |
1699 by (fact multiset_order.less_asym) |
1700 |
1700 |
1701 ML {* |
1701 ML {* |
1702 (* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *) |
|
1703 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) |
1702 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T])) |
1704 (Const _ $ t') = |
1703 (Const _ $ t') = |
1705 let |
1704 let |
1706 val (maybe_opt, ps) = |
1705 val (maybe_opt, ps) = |
1707 Nitpick_Model.dest_plain_fun t' ||> op ~~ |
1706 Nitpick_Model.dest_plain_fun t' ||> op ~~ |