equal
deleted
inserted
replaced
427 @{subgoals [display]} |
427 @{subgoals [display]} |
428 \end{minipage}*} |
428 \end{minipage}*} |
429 (*<*)oops(*>*) |
429 (*<*)oops(*>*) |
430 |
430 |
431 text {* |
431 text {* |
432 This tactic works however only if the quick-and-dirty mode of Isabelle |
|
433 is switched on. This is done automatically in the ``interactive |
|
434 mode'' of Isabelle, but must be done manually in the ``batch mode'' |
|
435 with the assignment |
|
436 *} |
|
437 |
|
438 ML{*quick_and_dirty := true*} |
|
439 |
|
440 text {* |
|
441 Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown |
432 Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown |
442 earlier, corresponds to the assumption method. |
433 earlier, corresponds to the assumption method. |
443 *} |
434 *} |
444 |
435 |
445 lemma |
436 lemma |