src/HOL/Transitive_Closure.thy
changeset 19656 09be06943252
parent 19623 12e6cc4382ae
child 20716 a6686a8e1b68
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -36,20 +36,19 @@
     1.4      r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
     1.5      trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
     1.6  
     1.7 -syntax
     1.8 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
     1.9 -translations
    1.10 -  "r^=" == "r \<union> Id"
    1.11 +abbreviation
    1.12 +  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    1.13 +  "r^= == r \<union> Id"
    1.14  
    1.15 -syntax (xsymbols)
    1.16 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
    1.17 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    1.18 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    1.19 +const_syntax (xsymbols)
    1.20 +  rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.21 +  trancl  ("(_\<^sup>+)" [1000] 999)
    1.22 +  reflcl  ("(_\<^sup>=)" [1000] 999)
    1.23  
    1.24 -syntax (HTML output)
    1.25 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
    1.26 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    1.27 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    1.28 +const_syntax (HTML output)
    1.29 +  rtrancl  ("(_\<^sup>*)" [1000] 999)
    1.30 +  trancl  ("(_\<^sup>+)" [1000] 999)
    1.31 +  reflcl  ("(_\<^sup>=)" [1000] 999)
    1.32  
    1.33  
    1.34  subsection {* Reflexive-transitive closure *}