equal
deleted
inserted
replaced
1473 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?) |
1473 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?) |
1474 |
1474 |
1475 (FIXME: @{ML ObjectLogic.full_atomize_tac}, |
1475 (FIXME: @{ML ObjectLogic.full_atomize_tac}, |
1476 @{ML ObjectLogic.rulify_tac}) |
1476 @{ML ObjectLogic.rulify_tac}) |
1477 |
1477 |
|
1478 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) |
|
1479 |
1478 *} |
1480 *} |
1479 |
1481 |
1480 section {* Simprocs *} |
1482 section {* Simprocs *} |
1481 |
1483 |
1482 text {* |
1484 text {* |