# HG changeset patch
# User blanchet
# Date 1390240793 -3600
# Node ID 558c9ceabaa107de58678efa4b805d8cabee9247
# Parent  4cf280104b85455676944e5c91e48df99901b01e
deactivate one more cardinal notation

diff -r 4cf280104b85 -r 558c9ceabaa1 src/HOL/Library/Cardinal_Notations.thy
--- a/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 18:25:44 2014 +0100
+++ b/src/HOL/Library/Cardinal_Notations.thy	Mon Jan 20 18:59:53 2014 +0100
@@ -16,6 +16,7 @@
   ordLeq3 (infix "\<le>o" 50) and
   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)
diff -r 4cf280104b85 -r 558c9ceabaa1 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:25:44 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:59:53 2014 +0100
@@ -27,6 +27,7 @@
   ordLeq3 (infix "\<le>o" 50) and
   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)