equal
deleted
inserted
replaced
186 \begin{isabelle} |
186 \begin{isabelle} |
187 ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
187 ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
188 \end{isabelle} |
188 \end{isabelle} |
189 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
189 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
190 ignored most of the time, or simply treated as a list of variables local to |
190 ignored most of the time, or simply treated as a list of variables local to |
191 this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}. |
191 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. |
192 The {\it assumptions} are the local assumptions for this subgoal and {\it |
192 The {\it assumptions} are the local assumptions for this subgoal and {\it |
193 conclusion} is the actual proposition to be proved. Typical proof steps |
193 conclusion} is the actual proposition to be proved. Typical proof steps |
194 that add new assumptions are induction or case distinction. In our example |
194 that add new assumptions are induction or case distinction. In our example |
195 the only assumption is the induction hypothesis @{term"rev (rev list) = |
195 the only assumption is the induction hypothesis @{term"rev (rev list) = |
196 list"}, where @{term"list"} is a variable name chosen by Isabelle. If there |
196 list"}, where @{term"list"} is a variable name chosen by Isabelle. If there |