src/HOL/Code_Evaluation.thy
changeset 81080 4aa4bd946f96
parent 80932 261cd8722677
child 81100 6ae3d0b2b8ad