1804 *}

  1804 *}

  1805 

  1805 

  1806 lemma 

  1806 lemma 

  1807   shows "Suc 0 = 1"

  1807   shows "Suc 0 = 1"

  1808 apply(simp)

  1808 apply(simp)

  1813   @{text "> The redex: Suc 0"}\\

  1812   @{text "> The redex: Suc 0"}\\

  1817   This will print out the message twice: once for the left-hand side and

  1816   This will print out the message twice: once for the left-hand side and

  1818   once for the right-hand side. The reason is that during simplification the

  1817   once for the right-hand side. The reason is that during simplification the

  1819   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc

  1818   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc

  1820   0"}, and then the simproc ``fires'' also on that term. 

  1819   0"}, and then the simproc ``fires'' also on that term. 

  1821 

  1820