src/HOL/Library/Cardinal_Notations.thy
changeset 55075 b3d0a02a756d
parent 55070 235c7661a96b
child 55078 558c9ceabaa1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Library/Cardinal_Notations.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2013
+
+Cardinal notations.
+*)
+
+header {* Cardinal Notations *}
+
+theory Cardinal_Notations
+imports Main
+begin
+
+notation
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90)
+
+end