src/HOL/Code_Evaluation.thy
changeset 66120 e03ff7e831cc
parent 66013 03002d10bf1d
child 68028 1f9f973eed2a