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 *}

  2542 *}

  2542 *}

  2543 

  2543 

  2544 

  2544 

  2545 section {* Declarations (TBD) *}

  2545 section {* Declarations (TBD) *}

  2546 

  2546 

  2548 

  2548 

  2549 text {* TBD *}

  2549 text {* TBD *}

  2550 

  2550 

  2551 lemma True

  2551 lemma True

  2552 proof

  2552 proof