src/Pure/Thy/thy_syntax.ML
changeset 57101 c881a983a19f
parent 55915 607948c90bf0
child 57105 bf5ddf4ec64b