wenzelm [Fri, 07 Nov 2014 22:15:51 +0100] rev 58936
eliminated pointless check -- command definitions are subject to theory context;
wenzelm [Fri, 07 Nov 2014 20:43:13 +0100] rev 58935
merged
wenzelm [Fri, 07 Nov 2014 20:06:18 +0100] rev 58934
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
tuned message;
wenzelm [Fri, 07 Nov 2014 19:47:05 +0100] rev 58933
tuned markup;
wenzelm [Fri, 07 Nov 2014 17:43:50 +0100] rev 58932
tuned;
wenzelm [Fri, 07 Nov 2014 17:31:01 +0100] rev 58931
clarified keyword categories;
tuned;
wenzelm [Fri, 07 Nov 2014 16:55:09 +0100] rev 58930
tuned signature;
wenzelm [Fri, 07 Nov 2014 16:51:36 +0100] rev 58929
tuned;
wenzelm [Fri, 07 Nov 2014 16:36:55 +0100] rev 58928
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
wenzelm [Fri, 07 Nov 2014 16:22:25 +0100] rev 58927
proper import for command 'permanent_interpretation';