src/HOL/Code_Evaluation.thy
changeset 57354 ded92100ffd7
parent 56928 1e50fddbe1f5
child 58036 f23045003476