Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
installing plus_ac0 for multisets
authorpaulson
Wed, 24 May 2000 18:42:28 +0200
changeset 8951 5483f52da41d
parent 8950 3e858b72fac9
child 8952 921c35be6ffb
installing plus_ac0 for multisets
src/HOL/Induct/MultisetOrder.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle