src/HOL/Import/import_rule.ML
changeset 59425 c5e79df8cc21
parent 58960 4bee6d8c1500
child 59582 0fbed69ff081
equal deleted inserted replaced
59424:ca2336984f6a 59425:c5e79df8cc21