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.
adding code attribute to enable evaluation of equality on multisets
authorbulwahn
Wed, 14 Dec 2011 15:56:29 +0100
changeset 45866 e62b319c7696
parent 45864 a8b9191609a8
child 45867 bce0a2089dfb
adding code attribute to enable evaluation of equality on multisets
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Dec 14 15:56:29 2011 +0100
@@ -1103,7 +1103,7 @@
 begin
 
 definition
-  "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
 
 instance proof
 qed (simp add: equal_multiset_def eq_iff)
isabelle