src/HOL/Code_Evaluation.thy
changeset 33756 47b7c9e0bf6e
parent 33632 6ea8a4cce9e7
child 34028 1e6206763036