equal
deleted
inserted
replaced
108 text {* |
108 text {* |
109 The syntax of the \simpleinductive{} command can be described by the |
109 The syntax of the \simpleinductive{} command can be described by the |
110 railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less |
110 railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less |
111 translates directly into the parser |
111 translates directly into the parser |
112 |
112 |
113 @{ML_chunk [display,gray] parser} |
113 @{ML_chunk [display,gray,linenos] parser} |
114 |
114 |
115 which we also described in Section~\ref{sec:parsingspecs} |
115 which we also described in Section~\ref{sec:parsingspecs} |
116 |
116 |
117 In order to add a new inductive predicate to a theory with the help of our |
117 In order to add a new inductive predicate to a theory with the help of our |
118 package, the user must \emph{invoke} it. For every package, there are |
118 package, the user must \emph{invoke} it. For every package, there are |