src/Pure/Thy/thy_syntax.ML
changeset 58918 8d36bc5eaed3
parent 58864 505a8150368a
child 58923 cb9b69cca999