src/HOL/Library/Cardinal_Notations.thy
2014-01-20 blanchet 2014-01-20 deactivate one more cardinal notation
2014-01-20 blanchet 2014-01-20 dissolved BNF session