# HG changeset patch
# User traytel
# Date 1367222615 -7200
# Node ID 5c53d40a8eed1f7e3efd0b40c83dbcbc54019a9f
# Parent  67757f1d5e7151baf7e909164429b978fc730c44
tuned operator precedence

diff -r 67757f1d5e71 -r 5c53d40a8eed src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Apr 29 09:45:14 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Apr 29 10:03:35 2013 +0200
@@ -366,10 +366,10 @@
 
 subsection {* Exponentiation *}
 
-definition cexp (infixr "^c" 80) where
+definition cexp (infixr "^c" 90) where
   "r1 ^c r2 \<equiv> |Func (Field r2) (Field r1)|"
 
-definition ccexp (infixr "^^c" 80) where
+definition ccexp (infixr "^^c" 90) where
   "r1 ^^c r2 \<equiv> |Pfunc (Field r2) (Field r1)|"
 
 lemma cexp_ordLeq_ccexp: "r1 ^c r2 \<le>o r1 ^^c r2"