src/Tools/try.ML
changeset 82454 ba1f9fb23b8d
parent 82360 6a09257afd06
equal deleted inserted replaced
82453:f9e6cbc6bf22 82454:ba1f9fb23b8d