src/HOL/Code_Evaluation.thy
changeset 40148 8728165d366e
parent 39567 5ee997fbe5cc
child 40638 6b137c96df07
equal deleted inserted replaced
40147:d170c322157a 40148:8728165d366e