src/HOL/Tools/code_evaluation.ML
changeset 63188 38d6aabec460
parent 63180 ddfd021884b4
child 63239 d562c9948dee
equal deleted inserted replaced
63187:da1cd3ce80c2 63188:38d6aabec460