src/Tools/code/code_name.ML
changeset 30441 193cf2fa692a
parent 30364 577edc39b501
child 30648 17365ef082f3
equal deleted inserted replaced
30439:57c68b3af2ea 30441:193cf2fa692a