src/HOL/Import/import_rule.ML
changeset 59859 f9d1442c70f3
parent 59621 291934bac95e
child 59936 b8ffc3dc9e24