src/Pure/Syntax/scan.ML
changeset 6109 82b50115564c
parent 5987 389d03e6e093
equal deleted inserted replaced
6108:2c9ed58c30ba 6109:82b50115564c