Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/SetsAndFunctions.thy
changeset 35267 8dfd816713c6
parent 30741 9e23e3ea7edd 
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Feb 19 14:47:00 2010 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Feb 19 14:47:01 2010 +0100
@@ -119,14 +119,14 @@
   apply (force simp add: mult_assoc)
   done
 
-interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
+interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
   apply default
    apply (unfold set_plus_def)
    apply (force simp add: add_ac)
   apply force
   done
 
-interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
+interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
   apply default
    apply (unfold set_times_def)
    apply (force simp add: mult_ac)
isabelle