hide 'csum' etc.
--- 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
--- 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