src/HOL/Import/import_rule.ML
changeset 59781 a71dbf3481a2
parent 59621 291934bac95e
child 59936 b8ffc3dc9e24