src/Pure/Isar/locale.ML
changeset 21350 6e58289b6685
parent 21264 14d4e7f78e46
child 21361 653d1631f997
equal deleted inserted replaced
21349:09c3af731e27 21350:6e58289b6685