src/HOL/Tools/code_evaluation.ML
changeset 40607 30d512bf47a7
parent 39567 5ee997fbe5cc
child 40726 16dcfedc4eb7
equal deleted inserted replaced
40606:af1a0b0c6202 40607:30d512bf47a7