src/HOL/Import/import_rule.ML
changeset 80418 9f90c4864e55
parent 79336 032a31db4c6f
child 81521 1bfad73ab115
equal deleted inserted replaced
80417:10ab5a74f6f5 80418:9f90c4864e55