src/Tools/try.ML
changeset 58904 f49c4f883c58
parent 58893 9e0ecb66d6a7
child 58923 cb9b69cca999
equal deleted inserted replaced
58903:38c72f5f6c2e 58904:f49c4f883c58