src/HOL/Transitive_Closure.thy
changeset 14361 ad2f5da643b4
parent 14337 e13731554e50
child 14398 c5c47703f763
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -39,9 +39,9 @@
     1.4    "r^=" == "r \<union> Id"
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>*)" [1000] 999)
     1.8 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>+)" [1000] 999)
     1.9 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    1.10 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
    1.11 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    1.12 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    1.13  
    1.14  
    1.15  subsection {* Reflexive-transitive closure *}