--- a/src/HOL/Trancl.thy Mon Aug 19 11:22:16 1996 +0200
+++ b/src/HOL/Trancl.thy Mon Aug 19 11:23:25 1996 +0200
@@ -8,19 +8,22 @@
rtrancl is reflexive/transitive closure;
trancl is transitive closure
reflcl is reflexive closure
+
+These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
+ atomic.
*)
Trancl = Lfp + Relation +
constdefs
- rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
+ rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 1000)
"r^* == lfp(%s. id Un (r O s))"
- trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
+ trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 1000)
"r^+ == r O rtrancl(r)"
syntax
- reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
+ reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [1000] 1000)
translations
"r^=" == "r Un id"