src/HOL/Code_Evaluation.thy
changeset 69148 d0517da45e5c
parent 68028 1f9f973eed2a
child 69605 a96320074298
equal deleted inserted replaced
69147:6f4d561ea621 69148:d0517da45e5c