equal
deleted
inserted
replaced
144 @{text "*** empty result sequence -- proof command failed"}\\ |
144 @{text "*** empty result sequence -- proof command failed"}\\ |
145 @{text "*** At command \"apply\"."} |
145 @{text "*** At command \"apply\"."} |
146 \end{isabelle} |
146 \end{isabelle} |
147 |
147 |
148 This means they failed.\footnote{To be precise tactics do not produce this error |
148 This means they failed.\footnote{To be precise tactics do not produce this error |
149 message, the it originates from the \isacommand{apply} wrapper.} The reason for this |
149 message, it originates from the \isacommand{apply} wrapper.} The reason for this |
150 error message is that tactics |
150 error message is that tactics |
151 are functions mapping a goal state to a (lazy) sequence of successor states. |
151 are functions mapping a goal state to a (lazy) sequence of successor states. |
152 Hence the type of a tactic is: |
152 Hence the type of a tactic is: |
153 *} |
153 *} |
154 |
154 |