doc-src/Functions/Thy/ROOT.ML
changeset 48610 0095de9e9da0
parent 48609 0090fab725e3
child 48611 b34ff75c23a7
equal deleted inserted replaced
48609:0090fab725e3 48610:0095de9e9da0
     1 use_thy "Functions";