src/HOL/Import/import_rule.ML
changeset 58315 6d8458bc6e27
parent 58239 1c5bc387bd4c
child 58960 4bee6d8c1500