equal
deleted
inserted
replaced
361 *} |
361 *} |
362 (*<*)oops(*>*) |
362 (*<*)oops(*>*) |
363 |
363 |
364 text {* |
364 text {* |
365 A simple tactic for easy discharge of any proof obligations is |
365 A simple tactic for easy discharge of any proof obligations is |
366 @{ML_ind cheat_tac in SkipProof}. This tactic corresponds to |
366 @{ML_ind cheat_tac in Skip_Proof}. This tactic corresponds to |
367 the Isabelle command \isacommand{sorry} and is sometimes useful |
367 the Isabelle command \isacommand{sorry} and is sometimes useful |
368 during the development of tactics. |
368 during the development of tactics. |
369 *} |
369 *} |
370 |
370 |
371 lemma shows "False" and "Goldbach_conjecture" |
371 lemma shows "False" and "Goldbach_conjecture" |
372 apply(tactic {* SkipProof.cheat_tac @{theory} *}) |
372 apply(tactic {* Skip_Proof.cheat_tac @{theory} *}) |
373 txt{*\begin{minipage}{\textwidth} |
373 txt{*\begin{minipage}{\textwidth} |
374 @{subgoals [display]} |
374 @{subgoals [display]} |
375 \end{minipage}*} |
375 \end{minipage}*} |
376 (*<*)oops(*>*) |
376 (*<*)oops(*>*) |
377 |
377 |