1468   After this, the simplifier is aware of the simproc and you can test whether 

  1468   After this, the simplifier is aware of the simproc and you can test whether 

  1469   it fires on the lemma:

  1469   it fires on the lemma:

  1470 *}

  1470 *}

  1471 

  1471 

  1472 lemma shows "Suc 0 = 1"

  1472 lemma shows "Suc 0 = 1"

  1474 (*<*)oops(*>*)

  1474 (*<*)oops(*>*)

  1475 

  1475 

  1476 text {*

  1476 text {*

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

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

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

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

  1491   interference from other rewrite rules, you can call @{text fail_sp} 

  1491   interference from other rewrite rules, you can call @{text fail_sp} 

  1492   as follows:

  1492   as follows:

  1493 *}

  1493 *}

  1494 

  1494 

  1495 lemma shows "Suc 0 = 1"

  1495 lemma shows "Suc 0 = 1"

  1497 (*<*)oops(*>*)

  1497 (*<*)oops(*>*)

  1498 

  1498 

  1499 text {*

  1499 text {*

  1500   Now the message shows up only once since the term @{term "1::nat"} is 

  1500   Now the message shows up only once since the term @{term "1::nat"} is 

  1501   left unchanged. 

  1501   left unchanged. 

  1502 

  1502 

  1504   always add automatically the simproc to the current simpset. If you do not

  1504   always add automatically the simproc to the current simpset. If you do not

  1505   want this, then you have to use a slightly different method for setting 

  1505   want this, then you have to use a slightly different method for setting 

  1506   up the simproc. First the function @{ML fail_sp_aux} needs to be modified

  1506   up the simproc. First the function @{ML fail_sp_aux} needs to be modified

  1507   to

  1507   to

  1508 *}

  1508 *}