# HG changeset patch
# User wenzelm
# Date 1727813531 -7200
# Node ID 2a8afc91ce9c5b4e235091256c8e125fd8bddbd8
# Parent  9b11062b62c6b2d7608ef4cdc6a12795feb2bbf8
more 'no_syntax' bundles;

diff -r 9b11062b62c6 -r 2a8afc91ce9c src/HOL/Transitive_Closure.thy
--- 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>