src/Tools/Code/code_simp.ML
changeset 38769 317e64c886d2
parent 38671 febcd1733229
child 38759 37a9092de102
equal deleted inserted replaced
38768:ecc713816e33 38769:317e64c886d2