equal
deleted
inserted
replaced
799 apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") |
799 apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") |
800 prefer 2 |
800 prefer 2 |
801 apply (rule one_step_implies_mult) |
801 apply (rule one_step_implies_mult) |
802 apply (simp only: trans_def) |
802 apply (simp only: trans_def) |
803 apply auto |
803 apply auto |
804 apply (blast intro: order_less_trans) |
|
805 done |
804 done |
806 |
805 |
807 theorem union_upper1: "A <= A + (B::'a::order multiset)" |
806 theorem union_upper1: "A <= A + (B::'a::order multiset)" |
808 apply (subgoal_tac "A + {#} <= A + B") |
807 apply (subgoal_tac "A + {#} <= A + B") |
809 prefer 2 |
808 prefer 2 |