equal
deleted
inserted
replaced
1590 (FIXME: What are the second components of the congruence rules---something to |
1590 (FIXME: What are the second components of the congruence rules---something to |
1591 do with weak congruence constants?) |
1591 do with weak congruence constants?) |
1592 |
1592 |
1593 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?) |
1593 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?) |
1594 |
1594 |
1595 (FIXME: @{ML ObjectLogic.full_atomize_tac}, |
|
1596 @{ML ObjectLogic.rulify_tac}) |
|
1597 |
|
1598 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) |
1595 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy) |
1599 |
1596 |
1600 (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.) |
1597 (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.) |
1601 |
1598 |
1602 *} |
1599 *} |