src/HOL/Transitive_Closure.thy
changeset 10331 7411e4659d4a
parent 10213 01c2744a3786
child 10565 7f7c1c3511e2
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:31:21 2000 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:32:02 2000 +0200
     1.3 @@ -9,23 +9,27 @@
     1.4  trancl  is transitive closure
     1.5  reflcl  is reflexive closure
     1.6  
     1.7 -These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
     1.8 -      atomic.
     1.9 +These postfix operators have MAXIMUM PRIORITY, forcing their operands
    1.10 +to be atomic.
    1.11  *)
    1.12  
    1.13  Transitive_Closure = Lfp + Relation + 
    1.14  
    1.15  constdefs
    1.16 -  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
    1.17 -  "r^*  ==  lfp(%s. Id Un (r O s))"
    1.18 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.19 +  "r^* == lfp (%s. Id Un (r O s))"
    1.20  
    1.21 -  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
    1.22 -  "r^+  ==  r O rtrancl(r)"
    1.23 +  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    1.24 +  "r^+ ==  r O rtrancl r"
    1.25  
    1.26  syntax
    1.27 -  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
    1.28 -
    1.29 +  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    1.30  translations
    1.31    "r^=" == "r Un Id"
    1.32  
    1.33 +syntax (xsymbols)
    1.34 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    1.35 +  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    1.36 +  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    1.37 +
    1.38  end