src/HOL/Tools/code_evaluation.ML
changeset 56852 b38c5b9cf590
parent 56245 84fc7dfa3cd4
child 56925 601edd9a6859
equal deleted inserted replaced
56851:35ff4ede3409 56852:b38c5b9cf590