src/HOL/Transitive_Closure.thy
changeset 14565 c6dc17aab88a
parent 14404 4952c5a92e04
child 15076 4b3d280ef06a
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -43,6 +43,11 @@
     1.4    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
     1.5    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
     1.9 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    1.10 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    1.11 +
    1.12  
    1.13  subsection {* Reflexive-transitive closure *}
    1.14