616   specifications of function definitions, inductive predicates and so on. In

   616   specifications of function definitions, inductive predicates and so on. In

   617   Chapter~\ref{chp:package}, for example, we will need to parse specifications

   617   Chapter~\ref{chp:package}, for example, we will need to parse specifications

   618   for inductive predicates of the form:

   618   for inductive predicates of the form:

   619 *}

   619 *}

   620 

   620 

   622 simple_inductive

   621 simple_inductive

   623   even and odd

   622   even and odd

   624 where

   623 where

   625   even0: "even 0"

   624   even0: "even 0"

   626 | evenS: "odd n \<Longrightarrow> even (Suc n)"

   625 | evenS: "odd n \<Longrightarrow> even (Suc n)"

   627 | oddS: "even n \<Longrightarrow> odd (Suc n)"

   626 | oddS: "even n \<Longrightarrow> odd (Suc n)"

   629 

   627 

   630 text {*

   628 text {*

   631   For this we are going to use the parser:

   629   For this we are going to use the parser:

   632 *}

   630 *}

   633 

   631