src/Pure/General/long_name.ML
changeset 81028 84f6f17274d0
parent 79319 2d9baa7ee05a
equal deleted inserted replaced
81027:a9dc66e05297 81028:84f6f17274d0