# HG changeset patch
# User wenzelm
# Date 1728420987 -7200
# Node ID d23f5a898084a86f53b5686095ef97fa88271f89
# Parent  072cc2a92ba3bb3b881b195d7f8efb7da3bb2d00
more syntax bundles;

diff -r 072cc2a92ba3 -r d23f5a898084 NEWS
--- a/NEWS	Tue Oct 08 17:26:31 2024 +0200
+++ b/NEWS	Tue Oct 08 22:56:27 2024 +0200
@@ -67,6 +67,8 @@
   unbundle no list_syntax
   unbundle no list_enumeration_syntax
   unbundle no list_comprehension_syntax
+  unbundle no relcomp_syntax
+  unbundle no converse_syntax
   unbundle no rtrancl_syntax
   unbundle no trancl_syntax
   unbundle no reflcl_syntax
diff -r 072cc2a92ba3 -r d23f5a898084 src/HOL/Examples/Coherent.thy
--- a/src/HOL/Examples/Coherent.thy	Tue Oct 08 17:26:31 2024 +0200
+++ b/src/HOL/Examples/Coherent.thy	Tue Oct 08 22:56:27 2024 +0200
@@ -11,7 +11,8 @@
 
 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
 
-no_notation comp  (infixl \<open>o\<close> 55) and relcomp  (infixr \<open>O\<close> 75)
+no_notation comp  (infixl \<open>o\<close> 55)
+unbundle no relcomp_syntax
 
 lemma p1p2:
   assumes "col a b c l \<and> col d e f m"
diff -r 072cc2a92ba3 -r d23f5a898084 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Oct 08 17:26:31 2024 +0200
+++ b/src/HOL/Relation.thy	Tue Oct 08 22:56:27 2024 +0200
@@ -969,11 +969,14 @@
 
 subsubsection \<open>Composition\<close>
 
-inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set"  (infixr \<open>O\<close> 75)
+inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set"
   for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
-  where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
+  where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> relcomp r s"
 
-notation relcompp (infixr \<open>OO\<close> 75)
+open_bundle relcomp_syntax
+begin
+notation relcomp  (infixr \<open>O\<close> 75) and relcompp  (infixr \<open>OO\<close> 75)
+end
 
 lemmas relcomppI = relcompp.intros
 
@@ -1074,15 +1077,19 @@
 
 subsubsection \<open>Converse\<close>
 
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"
   for r :: "('a \<times> 'b) set"
-  where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
+  where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> converse r"
 
-notation conversep  (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
-
+open_bundle converse_syntax
+begin
+notation
+  converse  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999) and
+  conversep  (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
 notation (ASCII)
   converse  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_^-1)\<close> [1000] 999) and
   conversep (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_^--1)\<close> [1000] 1000)
+end
 
 lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
   by (fact converse.intros)