src/HOL/Import/import_rule.ML
changeset 56812 baef1c110f12
parent 56267 deab4d428bc6
child 58239 1c5bc387bd4c