--- a/src/HOL/Transitive_Closure.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Transitive_Closure.thy Wed Apr 14 14:13:05 2004 +0200
@@ -43,6 +43,11 @@
trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
"_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+syntax (HTML output)
+ rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
+ trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
+ "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+
subsection {* Reflexive-transitive closure *}