equal
deleted
inserted
replaced
181 \begin{isabelle} |
181 \begin{isabelle} |
182 ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
182 ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
183 \end{isabelle} |
183 \end{isabelle} |
184 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
184 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
185 ignored most of the time, or simply treated as a list of variables local to |
185 ignored most of the time, or simply treated as a list of variables local to |
186 this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}. |
186 this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}. |
187 The {\it assumptions} are the local assumptions for this subgoal and {\it |
187 The {\it assumptions} are the local assumptions for this subgoal and {\it |
188 conclusion} is the actual proposition to be proved. Typical proof steps |
188 conclusion} is the actual proposition to be proved. Typical proof steps |
189 that add new assumptions are induction or case distinction. In our example |
189 that add new assumptions are induction or case distinction. In our example |
190 the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there |
190 the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there |
191 are multiple assumptions, they are enclosed in the bracket pair |
191 are multiple assumptions, they are enclosed in the bracket pair |