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 |
|
351 @{ML SkipProof.cheat_tac}. This tactic corresponds to |
|
352 the Isabelle command \isacommand{sorry} and is sometimes useful |
|
353 during the development of tactics. |
|
354 *} |
|
355 |
|
356 lemma shows "False" and "something_else_obviously_false" |
|
357 apply(tactic {* SkipProof.cheat_tac @{theory} *}) |
|
358 txt{*\begin{minipage}{\textwidth} |
|
359 @{subgoals [display]} |
|
360 \end{minipage}*} |
|
361 (*<*)oops(*>*) |
|
362 |
|
363 text {* |
350 Another simple tactic is the function @{ML atac}, which, as shown in the previous |
364 Another simple tactic is the function @{ML atac}, which, as shown in the previous |
351 section, corresponds to the assumption command. |
365 section, corresponds to the assumption command. |
352 *} |
366 *} |
353 |
367 |
354 lemma shows "P \<Longrightarrow> P" |
368 lemma shows "P \<Longrightarrow> P" |