equal
deleted
inserted
replaced
2480 have to construct quite large terms. Also see Recipe \ref{rec:timing} for information |
2480 have to construct quite large terms. Also see Recipe \ref{rec:timing} for information |
2481 about timing. |
2481 about timing. |
2482 \end{exercise} |
2482 \end{exercise} |
2483 |
2483 |
2484 \begin{readmore} |
2484 \begin{readmore} |
2485 See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. |
2485 See @{ML_file "Pure/conv.ML"} and @{ML_file "Tools/more_conv.ML"} |
|
2486 for more information about conversion combinators. |
2486 Some basic conversions are defined in @{ML_file "Pure/thm.ML"}, |
2487 Some basic conversions are defined in @{ML_file "Pure/thm.ML"}, |
2487 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. |
2488 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. |
2488 \end{readmore} |
2489 \end{readmore} |
2489 |
2490 |
2490 *} |
2491 *} |