src/HOL/Code_Evaluation.thy
changeset 82734 89347c0cc6a3
parent 81706 7beb0cf38292