src/HOL/Import/import_syntax.ML
changeset 38685 87a1e97a3ef3
parent 37165 c2e27ae53c2a
child 38803 38b68972721b