src/HOL/Code_Evaluation.thy
changeset 33085 c1b6cc29496b
parent 32740 9dd0a2f83429
child 33473 3b275a0bf18c
equal deleted inserted replaced
33083:1fad3160d873 33085:c1b6cc29496b