src/HOL/Import/import_rule.ML
changeset 59338 2ea1bf517842
parent 58960 4bee6d8c1500
child 59582 0fbed69ff081