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.
uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;
authorwenzelm
Wed, 09 Oct 2024 22:00:12 +0200
changeset 81140 e66172629fcc
parent 81139 d74e53f67474
child 81141 3e3e7a68cd80
uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;
src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Groups_Big.thy	Wed Oct 09 14:12:56 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Oct 09 22:00:12 2024 +0200
@@ -1415,8 +1415,8 @@
 sublocale prod: comm_monoid_set times 1
   defines prod = prod.F and prod' = prod.G ..
 
-abbreviation Prod (\<open>(\<open>open_block notation=\<open>prefix \<Prod>\<close>\<close>\<Prod>_)\<close> [1000] 999)
-  where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
+abbreviation Prod (\<open>\<Prod>\<close>)
+  where "\<Prod> \<equiv> prod (\<lambda>x. x)"
 
 end
isabelle