src/HOL/Tools/code_evaluation.ML
changeset 65512 9fd620f2fa7d
parent 65062 dc746d43f40e
child 66251 cd935b7cb3fb
equal deleted inserted replaced
65511:ea42dfd95ec8 65512:9fd620f2fa7d