src/HOL/Import/import_syntax.ML
changeset 23112 2bc882fbe51c
parent 22675 acf10be7dcca
child 23677 1114cc909800