src/HOL/ex/Commands.thy
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-12-04 wenzelm 2014-12-04 more examples;