src/Pure/Isar/locale.ML
changeset 43444 f744902b4681
parent 42375 774df7c59508
child 45290 f599ac41e7f5