src/HOL/Code_Evaluation.thy
changeset 66840 0d689d71dbdc
parent 66013 03002d10bf1d
child 68028 1f9f973eed2a