src/HOL/Code_Evaluation.thy
changeset 39733 6d373e9dcb9d
parent 39567 5ee997fbe5cc
child 40638 6b137c96df07