src/HOL/Code_Evaluation.thy
changeset 37367 8680677265c9
parent 36176 3fe7e97ccca8
child 38348 cf7b2121ad9d