src/HOL/Code_Evaluation.thy
changeset 40172 008dc2d2c395
parent 39567 5ee997fbe5cc
child 40638 6b137c96df07