equal
deleted
inserted
replaced
2136 |
2136 |
2137 \subsection{The Method {\tt\slshape insert}} |
2137 \subsection{The Method {\tt\slshape insert}} |
2138 |
2138 |
2139 \index{*insert (method)|(}% |
2139 \index{*insert (method)|(}% |
2140 The \isa{insert} method |
2140 The \isa{insert} method |
2141 inserts a given theorem as a new assumption of the current subgoal. This |
2141 inserts a given theorem as a new assumption of all subgoals. This |
2142 already is a forward step; moreover, we may (as always when using a |
2142 already is a forward step; moreover, we may (as always when using a |
2143 theorem) apply |
2143 theorem) apply |
2144 \isa{of}, \isa{THEN} and other directives. The new assumption can then |
2144 \isa{of}, \isa{THEN} and other directives. The new assumption can then |
2145 be used to help prove the subgoal. |
2145 be used to help prove the subgoals. |
2146 |
2146 |
2147 For example, consider this theorem about the divides relation. The first |
2147 For example, consider this theorem about the divides relation. The first |
2148 proof step inserts the distributive law for |
2148 proof step inserts the distributive law for |
2149 \isa{gcd}. We specify its variables as shown. |
2149 \isa{gcd}. We specify its variables as shown. |
2150 \begin{isabelle} |
2150 \begin{isabelle} |