src/HOL/Code_Evaluation.thy
changeset 37809 6c87cdad912d
parent 36176 3fe7e97ccca8
child 38348 cf7b2121ad9d