--- a/src/CCL/Trancl.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/CCL/Trancl.thy Fri Sep 20 19:51:08 2024 +0200
@@ -15,13 +15,13 @@
definition id :: "i set" (*the identity relation*)
where "id == {p. EX x. p = <x,x>}"
-definition relcomp :: "[i set,i set] \<Rightarrow> i set" (infixr "O" 60) (*composition of relations*)
+definition relcomp :: "[i set,i set] \<Rightarrow> i set" (infixr \<open>O\<close> 60) (*composition of relations*)
where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
-definition rtrancl :: "i set \<Rightarrow> i set" ("(_^*)" [100] 100)
+definition rtrancl :: "i set \<Rightarrow> i set" (\<open>(_^*)\<close> [100] 100)
where "r^* == lfp(\<lambda>s. id Un (r O s))"
-definition trancl :: "i set \<Rightarrow> i set" ("(_^+)" [100] 100)
+definition trancl :: "i set \<Rightarrow> i set" (\<open>(_^+)\<close> [100] 100)
where "r^+ == r O rtrancl(r)"