src/HOL/ex/Commands.thy
22 months ago wenzelm 2017-11-27 proper context (as in 'term' command);
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-12-04 wenzelm 2014-12-04 more examples;