doc-src/Exercises/2002/a5/ROOT.ML
changeset 15891 260090b54ef9
parent 15890 ff6787d730d5
child 15892 153541e29155
equal deleted inserted replaced
15890:ff6787d730d5 15891:260090b54ef9
     1 use_thy "a5";