src/HOL/Code_Evaluation.thy
changeset 74845 91ee232b4211
parent 72607 feebdaa346e5
child 80932 261cd8722677
equal deleted inserted replaced
74844:90242c744a1a 74845:91ee232b4211