src/HOL/Code_Evaluation.thy
changeset 81005 7846fa2c1c1e
parent 80932 261cd8722677
child 81100 6ae3d0b2b8ad