equal
deleted
inserted
replaced
360 |
360 |
361 text \<open> |
361 text \<open> |
362 This is all we need to let the conversion run against the simproc: |
362 This is all we need to let the conversion run against the simproc: |
363 \<close> |
363 \<close> |
364 |
364 |
365 ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context) |
365 ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) |
366 val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)\<close> |
366 (fn {context, ...} => c_tac context) |
|
367 val _ = Goal.prove @{context} [] [] (goal 8) |
|
368 (fn {context, ...} => s_tac context)\<close> |
367 |
369 |
368 text \<open> |
370 text \<open> |
369 If you do the exercise, you can see that both ways of simplifying additions |
371 If you do the exercise, you can see that both ways of simplifying additions |
370 perform relatively similar with perhaps some advantages for the |
372 perform relatively similar with perhaps some advantages for the |
371 simproc. That means the simplifier, even if much more complicated than |
373 simproc. That means the simplifier, even if much more complicated than |