src/HOL/Code_Evaluation.thy
changeset 66764 006deaf5c3dc
parent 66013 03002d10bf1d
child 68028 1f9f973eed2a