Re: [isabelle] defining "minor keywords"

On 16/06/18 16:45, Walther Neuper wrote:
> Reading structure Keyword and Pure.thy I conclude, that all keywords
> declared in Pure.thy remain "minor keywords" ("keywords" as seen by
> print_commands) unless they are explicitly made "commands" (as seen by
> print_commands) by "Outer_Syntax.command" and colleagues.>
> And I found no further way, to declare a "minor keyword" within
> Isabelle's user space, neither in the code nor in isar-ref.pdf.

The 'keywords' declaration works for both kinds of keywords: "keywords
foo" declares a minor keyword, "keywords bar :: kind" declares a major
(command) keyword.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.