358 

   358 

   359 

   359 

   360   The definition of the transitive closure should look as follows:

   360   The definition of the transitive closure should look as follows:

   361 *}

   361 *}

   362 

   362 

   363 text {*

   365 text {*

   364 

   366 

   365   A proposition can be parsed using the function @{ML prop in OuterParse}.

   367   A proposition can be parsed using the function @{ML prop in OuterParse}.

   366   Essentially, a proposition is just a string or an identifier, but using the

   368   Essentially, a proposition is just a string or an identifier, but using the

   367   specific parser function @{ML prop in OuterParse} leads to more instructive

   369   specific parser function @{ML prop in OuterParse} leads to more instructive

   375   In addition, the following function from @{ML_struct SpecParse} for parsing

   377   In addition, the following function from @{ML_struct SpecParse} for parsing

   376   an optional theorem name and attribute, followed by a delimiter, will be useful:

   378   an optional theorem name and attribute, followed by a delimiter, will be useful:

   377   

   379   

   378   \begin{table}

   380   \begin{table}

   379   @{ML "opt_thm_name:

   381   @{ML "opt_thm_name:

   381   \end{table}

   383   \end{table}

   382 

   384 

   383   We now have all the necessary tools to write the parser for our

   385   We now have all the necessary tools to write the parser for our

   384   \isa{\isacommand{simple{\isacharunderscore}inductive}} command:

   386   \isa{\isacommand{simple{\isacharunderscore}inductive}} command:

   385   

   387