src/HOL/Transitive_Closure.thy
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 21589 1b02201d7195
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -37,17 +37,17 @@
     1.4      trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
     1.5  
     1.6  abbreviation
     1.7 -  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
     1.8 +  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
     1.9    "r^= == r \<union> Id"
    1.10  
    1.11  notation (xsymbols)
    1.12 -  rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.13 -  trancl  ("(_\<^sup>+)" [1000] 999)
    1.14 +  rtrancl  ("(_\<^sup>*)" [1000] 999) and
    1.15 +  trancl  ("(_\<^sup>+)" [1000] 999) and
    1.16    reflcl  ("(_\<^sup>=)" [1000] 999)
    1.17  
    1.18  notation (HTML output)
    1.19 -  rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.20 -  trancl  ("(_\<^sup>+)" [1000] 999)
    1.21 +  rtrancl  ("(_\<^sup>*)" [1000] 999) and
    1.22 +  trancl  ("(_\<^sup>+)" [1000] 999) and
    1.23    reflcl  ("(_\<^sup>=)" [1000] 999)
    1.24  
    1.25