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/UNITY/Union.thy
changeset 81182 fc5066122e68
parent 80914 d97fdabd9e2b 
--- a/src/HOL/UNITY/Union.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/UNITY/Union.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -39,8 +39,8 @@
   where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> \<Union>(Acts ` X) \<longrightarrow> G \<in> X)"
 
 syntax
-  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              (\<open>(3\<Squnion>_./ _)\<close> 10)
-  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       (\<open>(3\<Squnion>_\<in>_./ _)\<close> 10)
+  "_JOIN1" :: "[pttrns, 'b set] => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> 10)
+  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> 10)
 syntax_consts
   "_JOIN1" "_JOIN" == JOIN
 translations
isabelle