--- a/src/HOL/Transitive_Closure.thy Tue Oct 01 21:35:31 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Oct 01 22:12:11 2024 +0200
@@ -64,6 +64,36 @@
tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
+bundle no_rtrancl_syntax
+begin
+no_notation
+ rtrancl (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999) and
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000)
+no_notation (ASCII)
+ rtrancl (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000)
+end
+
+bundle no_trancl_syntax
+begin
+no_notation
+ trancl (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
+no_notation (ASCII)
+ trancl (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000)
+end
+
+bundle no_reflcl_syntax
+begin
+no_notation
+ reflcl (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999) and
+ reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
+no_notation (ASCII)
+ reflcl (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
+ reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
+end
+
subsection \<open>Reflexive closure\<close>