src/HOL/Import/import_rule.ML
changeset 56982 51d4189d95cf
parent 56267 deab4d428bc6
child 58239 1c5bc387bd4c