523   OuterParse.prop input

   523   OuterParse.prop input

   524 end*}

   524 end*}

   525 

   525 

   526 text {* (FIXME funny output for a proposition) *}

   526 text {* (FIXME funny output for a proposition) *}

   527 

   527 

   529 

   529 

   530 text {*

   530 text {*

   531   There are a number of special purpose parsers that help with parsing specifications

   531   There are a number of special purpose parsers that help with parsing specifications

   532   of functions, inductive definitions and so on. For example the 

   532   of functions, inductive definitions and so on. For example the 

   533   @{ML OuterParse.target} reads a target in order to indicate a locale.

   533   @{ML OuterParse.target} reads a target in order to indicate a locale.