src/HOL/Code_Evaluation.thy
changeset 78366 aa4ea5398ab8
parent 72607 feebdaa346e5
child 80932 261cd8722677
equal deleted inserted replaced
78365:bb5e2a7198e3 78366:aa4ea5398ab8