src/HOL/Tools/code_evaluation.ML
changeset 40898 882e860a1e83
parent 40726 16dcfedc4eb7
child 41184 5c6f44d22f51
equal deleted inserted replaced
40897:1eb1b2f9d062 40898:882e860a1e83