# 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 "\o" 50) and ordLess2 (infix "o" 50) and ordLess2 (infix "