src/Tools/Code/code_simp.ML
changeset 53977 a7add756b9d2
parent 53437 b098d53152d9
child 54895 515630483010
equal deleted inserted replaced
53976:da610b507799 53977:a7add756b9d2