# HG changeset patch # User paulson # Date 958991702 -7200 # Node ID 433843c1b454dcd5d7b7bf3ca9adedb65b215607 # Parent 80303d9b0d7b921d28183f9e20e626933c39c5cc multisets are partially ordered diff -r 80303d9b0d7b -r 433843c1b454 src/HOL/Induct/MultisetOrder.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Induct/MultisetOrder.thy Mon May 22 12:35:02 2000 +0200 @@ -0,0 +1,14 @@ +(* Title: HOL/UNITY/MultisetOrder + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + +Multisets are partially ordered +*) + +MultisetOrder = Multiset + + +instance multiset :: (order) order + (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le) + +end