src/HOL/Code_Evaluation.thy
changeset 66428 745a43ff2d5f
parent 66013 03002d10bf1d
child 68028 1f9f973eed2a