src/Pure/Isar/locale.ML
changeset 31871 cc1486840914
parent 30777 9960ff945c52
child 31988 801aabf9f376
equal deleted inserted replaced
31870:5274d3d0a6f2 31871:cc1486840914