src/HOL/Code_Evaluation.thy
changeset 72907 3883f536d84d
parent 72607 feebdaa346e5
equal deleted inserted replaced
72906:00399e5a6e50 72907:3883f536d84d