src/HOL/Code_Evaluation.thy
changeset 57874 9c361f94b323
parent 56928 1e50fddbe1f5
child 58036 f23045003476