# HG changeset patch
# User blanchet
# Date 1390500142 -3600
# Node ID 6e16d2dd4f1417aa085f1d4a6273657d17e69eb6
# Parent  11408b65e9a6676339ed4ebe555e93ced84c9de9
hide 'csum' etc.

diff -r 11408b65e9a6 -r 6e16d2dd4f14 src/HOL/Library/Cardinal_Notations.thy
--- a/src/HOL/Library/Cardinal_Notations.thy	Thu Jan 23 16:09:28 2014 +0100
+++ b/src/HOL/Library/Cardinal_Notations.thy	Thu Jan 23 19:02:22 2014 +0100
@@ -17,8 +17,13 @@
   ordLess2 (infix "<o" 50) and
   ordIso2 (infix "=o" 50) and
   card_of ("|_|") and
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90)
+  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
+  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
+  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
+
+abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
+abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
+abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
+abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
 
 end
diff -r 11408b65e9a6 -r 6e16d2dd4f14 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Jan 23 16:09:28 2014 +0100
+++ b/src/HOL/Main.thy	Thu Jan 23 19:02:22 2014 +0100
@@ -29,6 +29,7 @@
   convol ("<_ , _>")
 
 hide_const (open)
+  czero cinfinite cfinite csum cone ctwo Csum cprod cexp
   image2 image2p vimage2p Gr Grp collect fsts snds setl setr
   convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
   prefCl PrefCl Succ Shift shift proj