src/HOL/Transitive_Closure.thy
changeset 21210 c17fd2df4e9e
parent 20716 a6686a8e1b68
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -40,12 +40,12 @@
     1.4    reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
     1.5    "r^= == r \<union> Id"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.10    trancl  ("(_\<^sup>+)" [1000] 999)
    1.11    reflcl  ("(_\<^sup>=)" [1000] 999)
    1.12  
    1.13 -const_syntax (HTML output)
    1.14 +notation (HTML output)
    1.15    rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.16    trancl  ("(_\<^sup>+)" [1000] 999)
    1.17    reflcl  ("(_\<^sup>=)" [1000] 999)