src/HOL/Import/import_syntax.ML
changeset 17076 c7effdf2e2e2
parent 17057 0934ac31985f
child 17370 754b7fcff03e