src/HOL/Import/import_rule.ML
changeset 59637 f643308472ce
parent 59621 291934bac95e
child 59936 b8ffc3dc9e24