# HG changeset patch
# User paulson
# Date 840446605 -7200
# Node ID 43521f79f01698064f442d3e09503f25ea92527e
# Parent  7cd464e3e3c65720884a7a684fc1e0ef19969df2
Changed precedences to remove ambiguities in r^+ notation

diff -r 7cd464e3e3c6 -r 43521f79f016 src/HOL/Trancl.thy
--- 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"