src/Tools/Code/code_simp.ML
changeset 75319 c7ff16398535
parent 74561 8e6c973003c8
equal deleted inserted replaced
75318:a2c5efb7298a 75319:c7ff16398535