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 definition of equality of finite sets for executability of equality of finite sets
authorbulwahn
Tue, 07 Sep 2010 11:51:53 +0200
changeset 39190 a2775776be3f
parent 39189 d183bf90dabd
child 39191 edaf5a6ffa99
adding code attribute to definition of equality of finite sets for executability of equality of finite sets
src/HOL/Library/Fset.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Fset.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -230,7 +230,7 @@
 instantiation fset :: (type) equal
 begin
 
-definition
+definition [code]:
   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
 
 instance proof
isabelle