546 

   546 

   547 *}

   547 *}

   548 

   548 

   549 ML{* OuterSyntax.command *}

   549 ML{* OuterSyntax.command *}

   550 

   550 

   552 

   552 

   553 text {*

   553 text {*

   554   Often new commands, for example for providing new definitional principles,

   554   Often new commands, for example for providing new definitional principles,

   555   need to be implemented. While this is not difficult on the ML-level,

   555   need to be implemented. While this is not difficult on the ML-level,

   556   new commands, in order to be useful, need to be recognised by

   556   new commands, in order to be useful, need to be recognised by