doc-src/TutorialI/settings.ML
changeset 33145 1a22f7ca1dfc
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
33144:1831516747d4 33145:1a22f7ca1dfc