src/HOL/Code_Evaluation.thy
changeset 78764 a3dcae9a2ebe
parent 72607 feebdaa346e5
child 80932 261cd8722677
equal deleted inserted replaced
78763:b7157c137855 78764:a3dcae9a2ebe