src/Tools/Code/code_simp.ML
changeset 37891 c26f9d06e82c
parent 37839 b77e521e9f50
child 38669 9ff76d0f0610
equal deleted inserted replaced
37890:aae46a9ef66c 37891:c26f9d06e82c