src/HOL/Induct/MultisetOrder.thy
changeset 10258 d549f2534e6d
parent 10257 21055ac27708
child 10259 93ec82d535f2
     1.1 --- a/src/HOL/Induct/MultisetOrder.thy	Wed Oct 18 23:35:56 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,28 +0,0 @@
     1.4 -(*  Title:      HOL/Induct/MultisetOrder.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2000  University of Cambridge
     1.8 -
     1.9 -Multisets are partially ordered.
    1.10 -*)
    1.11 -
    1.12 -theory MultisetOrder = Multiset:
    1.13 -
    1.14 -instance multiset :: (order) order
    1.15 -  apply intro_classes
    1.16 -     apply (rule mult_le_refl)
    1.17 -    apply (erule mult_le_trans)
    1.18 -    apply assumption
    1.19 -   apply (erule mult_le_antisym)
    1.20 -   apply assumption
    1.21 -  apply (rule mult_less_le)
    1.22 -  done
    1.23 -
    1.24 -instance multiset :: ("term") plus_ac0
    1.25 -  apply intro_classes
    1.26 -    apply (rule union_commute)
    1.27 -   apply (rule union_assoc)
    1.28 -  apply simp
    1.29 -  done
    1.30 -
    1.31 -end