equal
deleted
inserted
replaced
345 \end{minipage} |
345 \end{minipage} |
346 *} |
346 *} |
347 (*<*)oops(*>*) |
347 (*<*)oops(*>*) |
348 |
348 |
349 text {* |
349 text {* |
350 A simple tactic making theorem proving particularly simple is |
350 A simple tactic for ``easily'' discharging proof obligations is |
351 @{ML SkipProof.cheat_tac}. This tactic corresponds to |
351 @{ML SkipProof.cheat_tac}. This tactic corresponds to |
352 the Isabelle command \isacommand{sorry} and is sometimes useful |
352 the Isabelle command \isacommand{sorry} and is sometimes useful |
353 during the development of tactics. |
353 during the development of tactics. |
354 *} |
354 *} |
355 |
355 |