src/HOL/Code_Evaluation.thy
changeset 39150 c4ff5fd8db99
parent 38857 97775f3e8722
child 39274 b17ffa965223