# HG changeset patch
# User paulson
# Date 959186548 -7200
# Node ID 5483f52da41d27bbfcdada69e939fce46c97c53e
# Parent  3e858b72fac98adfe043d71866a968c7d88247e1
installing plus_ac0 for multisets

diff -r 3e858b72fac9 -r 5483f52da41d src/HOL/Induct/MultisetOrder.thy
--- a/src/HOL/Induct/MultisetOrder.thy	Wed May 24 18:41:49 2000 +0200
+++ b/src/HOL/Induct/MultisetOrder.thy	Wed May 24 18:42:28 2000 +0200
@@ -11,4 +11,5 @@
 instance multiset :: (order) order
     (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le)
 
+instance multiset :: (term) plus_ac0 (union_comm,union_assoc) {|Auto_tac|}
 end