--- a/src/HOL/Transitive_Closure.thy Wed Oct 25 18:31:21 2000 +0200
+++ b/src/HOL/Transitive_Closure.thy Wed Oct 25 18:32:02 2000 +0200
@@ -9,23 +9,27 @@
trancl is transitive closure
reflcl is reflexive closure
-These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
- atomic.
+These postfix operators have MAXIMUM PRIORITY, forcing their operands
+to be atomic.
*)
Transitive_Closure = Lfp + Relation +
constdefs
- rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 999)
- "r^* == lfp(%s. Id Un (r O s))"
+ rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999)
+ "r^* == lfp (%s. Id Un (r O s))"
- trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 999)
- "r^+ == r O rtrancl(r)"
+ trancl :: "('a * 'a) set => ('a * 'a) set" ("(_^+)" [1000] 999)
+ "r^+ == r O rtrancl r"
syntax
- "_reflcl" :: "('a*'a)set => ('a*'a)set" ("(_^=)" [1000] 999)
-
+ "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_^=)" [1000] 999)
translations
"r^=" == "r Un Id"
+syntax (xsymbols)
+ rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999)
+ trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999)
+ "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999)
+
end