src/HOL/Code_Evaluation.thy
changeset 82203 c535cfba16db
parent 81706 7beb0cf38292
child 82900 bd3685e5f883
equal deleted inserted replaced
82202:a1f85f579a07 82203:c535cfba16db