equal
deleted
inserted
replaced
133 \begin{exercise} |
133 \begin{exercise} |
134 In Section~\ref{sec:nutshell} we required that introduction rules must be of the |
134 In Section~\ref{sec:nutshell} we required that introduction rules must be of the |
135 form |
135 form |
136 |
136 |
137 \begin{isabelle} |
137 \begin{isabelle} |
138 @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
138 @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"} |
139 \end{isabelle} |
139 \end{isabelle} |
140 |
140 |
141 where the @{text "As"} and @{text "Bs"} can be any collection of formulae |
141 where the @{text "As"} and @{text "Bs"} can be any collection of formulae |
142 not containing the @{text "preds"}. This requirement is important, |
142 not containing the @{text "preds"}. This requirement is important, |
143 because if violated, the theory behind the inductive package does not work |
143 because if violated, the theory behind the inductive package does not work |