src/HOL/Code_Evaluation.thy
changeset 40710 499aa989fbad
parent 40638 6b137c96df07
child 40883 b37dca06477f