src/HOL/Code_Evaluation.thy
changeset 32777 8ae3a48c69d9
parent 32740 9dd0a2f83429
child 33473 3b275a0bf18c