src/Pure/Isar/locale.ML
changeset 71751 abf3e80bd815
parent 71166 c9433e8e314e
child 72505 974071d873ba