21   modified in a sequence of proof steps until all of them are discharged.

    21   modified in a sequence of proof steps until all of them are discharged.

    22   In this chapter we will explain simple tactics and how to combine them using

    22   In this chapter we will explain simple tactics and how to combine them using

    23   tactic combinators. We also describe the simplifier, simprocs and conversions.

    23   tactic combinators. We also describe the simplifier, simprocs and conversions.

    24 *}

    24 *}

    25 

    25 

    27 

    27 

    28 text {*

    28 text {*

    29   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 

    29   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 

    30   into ML. Suppose the following proof.

    30   into ML. Suppose the following proof.

    31 *}

    31 *}

  2541 *}

  2541 *}

  2542 

  2542 

  2543 

  2543 

  2544 section {* Declarations (TBD) *}

  2544 section {* Declarations (TBD) *}

  2545 

  2545 

  2547 

  2547 

  2548 text {* TBD *}

  2548 text {* TBD *}

  2549 

  2549 

  2550 lemma True

  2550 lemma True

  2551 proof

  2551 proof