745   Both parsers accept the same input, but if you look closely, you can notice 

   745   Both parsers accept the same input, but if you look closely, you can notice 

   746   an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of 

   746   an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of 

   747   this additional ``tail''?

   747   this additional ``tail''?

   748   \end{exercise}

   748   \end{exercise}

   749 *}

   749 *}

   750 

   755 

   751 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   756 section {* New Commands and Keyword Files\label{sec:newcommand} *}

   752 

   757 

   753 text {*

   758 text {*

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

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