equal
deleted
inserted
replaced
1482 simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *} |
1482 simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *} |
1483 |
1483 |
1484 text {* |
1484 text {* |
1485 where the second argument specifies the pattern and the right-hand side |
1485 where the second argument specifies the pattern and the right-hand side |
1486 contains the code of the simproc (we have to use @{ML K} since we ignoring |
1486 contains the code of the simproc (we have to use @{ML K} since we ignoring |
1487 an argument about morphisms\footnote{FIXME: what does the morphism do?}). |
1487 an argument about morphisms. |
1488 After this, the simplifier is aware of the simproc and you can test whether |
1488 After this, the simplifier is aware of the simproc and you can test whether |
1489 it fires on the lemma: |
1489 it fires on the lemma: |
1490 *} |
1490 *} |
1491 |
1491 |
1492 lemma shows "Suc 0 = 1" |
1492 lemma shows "Suc 0 = 1" |