src/HOL/Import/import_rule.ML
changeset 58839 ccda99401bc8
parent 58239 1c5bc387bd4c
child 58960 4bee6d8c1500