136 \end{description} |
136 \end{description} |
137 Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on |
137 Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on |
138 the problematic subgoal above. |
138 the problematic subgoal above. |
139 Only one of the modifiers is allowed, and it must precede all |
139 Only one of the modifiers is allowed, and it must precede all |
140 other modifiers. |
140 other modifiers. |
141 |
141 %\begin{warn} |
142 \begin{warn} |
142 %Assumptions are simplified in a left-to-right fashion. If an |
143 Assumptions are simplified in a left-to-right fashion. If an |
143 %assumption can help in simplifying one to the left of it, this may get |
144 assumption can help in simplifying one to the left of it, this may get |
144 %overlooked. In such cases you have to rotate the assumptions explicitly: |
145 overlooked. In such cases you have to rotate the assumptions explicitly: |
145 %\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"} |
146 \isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"} |
146 %causes a cyclic shift by $n$ positions from right to left, if $n$ is |
147 causes a cyclic shift by $n$ positions from right to left, if $n$ is |
147 %positive, and from left to right, if $n$ is negative. |
148 positive, and from left to right, if $n$ is negative. |
148 %Beware that such rotations make proofs quite brittle. |
149 Beware that such rotations make proofs quite brittle. |
149 %\end{warn} |
150 \end{warn} |
|
151 *} |
150 *} |
152 |
151 |
153 subsection{*Rewriting with Definitions*} |
152 subsection{*Rewriting with Definitions*} |
154 |
153 |
155 text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions} |
154 text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions} |