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/ZF/UNITY/Union.thy
changeset 80917 2a77bc3b4eac
parent 80761 bc936d3d8b45 
--- a/src/ZF/UNITY/Union.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Union.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -41,8 +41,8 @@
       SKIP \<in> X \<and> (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
 
 syntax
-  "_JOIN1"  :: "[pttrns, i] \<Rightarrow> i"     (\<open>(3\<Squnion>_./ _)\<close> 10)
-  "_JOIN"   :: "[pttrn, i, i] \<Rightarrow> i"   (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
+  "_JOIN1"  :: "[pttrns, i] \<Rightarrow> i"     (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> 10)
+  "_JOIN"   :: "[pttrn, i, i] \<Rightarrow> i"   (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<in>\<close>\<close>\<Squnion>_ \<in> _./ _)\<close> 10)
 syntax_consts
   "_JOIN1" "_JOIN" == JOIN
 translations
isabelle