src/Tools/Code/code_simp.ML
changeset 45195 63ce9e743734
parent 43619 3803869014aa
child 45620 f2a587696afb
equal deleted inserted replaced
45194:d825a8f1d088 45195:63ce9e743734