src/HOL/Tools/code_evaluation.ML
changeset 56717 d96b10ec397c
parent 56245 84fc7dfa3cd4
child 56925 601edd9a6859
equal deleted inserted replaced
56716:6d5733303a50 56717:d96b10ec397c