diff -r 56f1c0af602c -r 8e72f55295fd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Relation.thy	Mon Sep 23 21:09:23 2024 +0200
@@ -1074,15 +1074,15 @@
 
 subsubsection \<open>Converse\<close>
 
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  (\<open>(_\<inverse>)\<close> [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix -1\<close>\<close>_\<inverse>)\<close> [1000] 999)
   for r :: "('a \<times> 'b) set"
   where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
 
-notation conversep  (\<open>(_\<inverse>\<inverse>)\<close> [1000] 1000)
+notation conversep  (\<open>(\<open>notation=\<open>postfix -1-1\<close>\<close>_\<inverse>\<inverse>)\<close> [1000] 1000)
 
 notation (ASCII)
-  converse  (\<open>(_^-1)\<close> [1000] 999) and
-  conversep (\<open>(_^--1)\<close> [1000] 1000)
+  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)
 
 lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
   by (fact converse.intros)