src/Pure/Isar/outer_syntax.ML
changeset 57978 8f4a332500e4
parent 57623 249c0297cf10
child 57905 c0c5652e796e