src/HOL/Tools/code_evaluation.ML
changeset 60690 a9e45c9588c3
parent 59621 291934bac95e
child 60801 7664e0916eec
equal deleted inserted replaced
60689:8a2d7c04d8c0 60690:a9e45c9588c3