equal
deleted
inserted
replaced
1194 @{subgoals[display]} |
1194 @{subgoals[display]} |
1195 *} |
1195 *} |
1196 (*<*)oops(*>*) |
1196 (*<*)oops(*>*) |
1197 |
1197 |
1198 text {* |
1198 text {* |
1199 As usual with simplification you have to worry about looping: you already have |
1199 As usual with rewriting you have to worry about looping: you already have |
1200 a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because |
1200 a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because |
1201 the default simpset contains a rule which just does the opposite of @{ML plus_one_sp}, |
1201 the default simpset contains a rule which just does the opposite of @{ML plus_one_sp}, |
1202 namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful |
1202 namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful |
1203 in choosing the right simpset to which you add a simproc. |
1203 in choosing the right simpset to which you add a simproc. |
1204 |
1204 |