# HG changeset patch
# User nipkow
# Date 868019850 -7200
# Node ID ce1664057431f6c4731f7de2d07d7f88d4ab7b84
# Parent  807549666b9c81ac6e151d34fa2e06bf815b8162
Reduced priority of postfix ^* etc operators such that they are the same as
application. Eg wf r^* now needs to be written wf(r^*).

diff -r 807549666b9c -r ce1664057431 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Jul 04 12:36:00 1997 +0200
+++ b/src/HOL/Relation.thy	Fri Jul 04 14:37:30 1997 +0200
@@ -9,7 +9,7 @@
     id          :: "('a * 'a)set"               (*the identity relation*)
     O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
-    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 1000)
+    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
     "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
     Domain      :: "('a*'b) set => 'a set"
     Range       :: "('a*'b) set => 'b set"
diff -r 807549666b9c -r ce1664057431 src/HOL/Trancl.thy
--- a/src/HOL/Trancl.thy	Fri Jul 04 12:36:00 1997 +0200
+++ b/src/HOL/Trancl.thy	Fri Jul 04 14:37:30 1997 +0200
@@ -16,14 +16,14 @@
 Trancl = Lfp + Relation + 
 
 constdefs
-  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 1000)
+  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] 1000)
+  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
   "r^+  ==  r O rtrancl(r)"
 
 syntax
-  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 1000)
+  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
 
 translations
   "r^=" == "r Un id"